计算机科学 ›› 2021, Vol. 48 ›› Issue (4): 31-36.doi: 10.11896/jsjkx.200500036
石铁柱, 钱俊彦, 潘海玉
SHI Tie-zhu, QIAN Jun-yan, PAN Hai-yu
摘要： 形式规约使用形式语言构建所开发的软硬件系统的规约,刻画系统的模型和性质。其中,性质规约中的分支时间规约对于系统验证有着非常重要的作用。在经典情形下,系统性质规约是基于二值逻辑的,不能描述不一致或不确定的信息。因此,将其推广到模糊逻辑背景下,有助于对模糊系统进行形式验证。文中首先给出了性质规约中分支时间属性在模糊背景下的形式化定义,重点研究了其中的安全性和活性;然后,定义了两种闭包操作,从而产生了4种类型的属性,即泛安全性、泛活性、存在安全性和存在活性;最后,证明了每个分支时间属性,或是存在安全性和存在活性的交,或是泛安全性和泛活性的交,或是存在安全性和泛活性的交。
中图分类号:
| [1]WANG J,ZHAN N J,FENG X Y,et al.Overview of formal methods[J].Journal of Software,2019,30(1):33-61. [2]BAIER C,KATOEN J P.Principles of model checking[M].Cambridge,MA: The MIT Press,2008. [3]LIN H M,ZHANG W H.Model checking: theories,techniques and applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912. [4]WANG Z Z.Survey of Model Checking[J].Computer Science,2013,40(Z6):1-14. [5]WEI O,SHI Y F,XU B F,et al.Abstract Modeling Formalisms in Software Model Checking[J].Journal of Computer Research and Development,2015,52(7):1580-1603. [6]HAN Y J,ZHOU Q L,ZHU W J.Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking[J].Computer Science,2019,46(11):25-31. [7]LIU Y,LI X D,MA Y.Model abstraction for stochastic modelchecking[J].Journal of Software,2015,26(8):1853-1870. [8]LIU Y,LI X D,MA Y,et al.Survey for Stochastic Model Checking[J].Chinese Jour-nal of Computers,2015,38(11):2145-2162. [9]CHECHIK M,DEVEREUX B,EASTERBRO-OK S,et al.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408. [10]LI Y M.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320:17-39. [11]DENG H,XUE Y,LI Y L,et al.Computation Tree Logic CTL*Based on Possibility Measure and Possibilistic Bisimulation[J].Computer Science,2012,39(10):258-263. [12]LEI L H,WANG J.Parallelization of LTL model checking based on possibility measure [J].Computer Science,2018,45(4):71-75. [13]PAN H Y,LI Y M,CAO Y Z,et al.Model checking fuzzy computation tree logic[J].Fuzzy Sets and Systems,2015,262:60-77. [14]PAN H Y,LI Y M,CAO Y Z,et al.Model checking computation tree logic over finite lattices[J].Theoretical Computer Scie-nce,2016,612(C):45-62. [15]LIANG C J,LI Y M.Model checking of fuzzy linear temporal logic based on generalized possibility measures[J].Acta Electronica Sinica,2017,45(12):2971-2977. [16]FARAN R,KUPFERMAN O.Spanning the spectrum fromsafety to liveness[J].Acta Informatica,2018,55(8):703-732. [17]ALPERN B,DEMERS A J,SCHNEIDER F B.Safety without stuttering[J].Information Proce-ssing Letters,1986,23(4):177-180. [18]KUPFERMAN O,VARDI M Y.Model checking of safetyproperties[J].Formal Methods in System Design,2001,19(3):291-314. [19]LAMPORT L.Proving the Correctness of Multip-rocess Pro-grams[J].IEEE Transactions on Software Engineering,1977,SE-3(2):125-143. [20]ALPERN B,SCHNEIDER F B.Defining liveness[J].Information Processing Letters,1985,21(4):181-185. [21]ALPERN B,SCHNEIDER F B.Recognizing safety and liveness[J].Distributed Computing,1987,2(3):117-126. [22]SISTLA A P.Safety,liveness and fairness in temporal logic[J].Formal Aspects of Computing,1994,6(5):495-511. [23]LI Y M,DROSTE M,LEI L H.Model checkin-g of linear-time properties in multi-valued systems[J].Information Sciences,2017,377:51-74. [24]MANOLIOS P,TTEFLER R.Safety and liven-ess in branching time[C]//In LICS.IEEE Computer Society,2001:366-374. [25]BOUAJJANI A,FERNANDEZ J C.Safety for branching time semantics[C]//18th ICALP.LNCS 510,1991:76-92. [26]KATOEN J P,LEI S,ZHANG L.Probably safe or live[C]//Eacsl Conference on Computer Science Logic.2014:1-10. [27]ZHANG X H,WU D P,DAI J H.Fuzzy Mathematics andRough Set Theory[M].Beijing: Tsinghua University Press,2012. [28]MANTACI S,RESTIVO A.Codes and equations on trees [J].Theoretical Computer Science,2001,255(1／2):483-509. |
| [1] | 周连兵, 周湘贞, 崔学荣. 基于双重二维混沌映射的压缩图像加密方案 Compressed Image Encryption Scheme Based on Dual Two Dimensional Chaotic Map 计算机科学, 2022, 49(8): 344-349. https://doi.org/10.11896/jsjkx.210700235 |
| [2] | 李瑭, 秦小麟, 迟贺宇, 费珂. 面向多无人系统的安全协同模型 Secure Coordination Model for Multiple Unmanned Systems 计算机科学, 2022, 49(7): 332-339. https://doi.org/10.11896/jsjkx.210600107 |
| [3] | 张振超, 刘亚丽, 殷新春. 适用于物联网环境的无证书广义签密方案 New Certificateless Generalized Signcryption Scheme for Internet of Things Environment 计算机科学, 2022, 49(3): 329-337. https://doi.org/10.11896/jsjkx.201200256 |
| [4] | 陈海彪, 黄声勇, 蔡洁锐. 一个基于智能电网的跨层路由的信任评估协议 Trust Evaluation Protocol for Cross-layer Routing Based on Smart Grid 计算机科学, 2021, 48(6A): 491-497. https://doi.org/10.11896/jsjkx.201000169 |
| [5] | 姜昊堃, 董学东, 张成. 改进的具有前向安全性的无证书代理盲签名方案 Improved Certificateless Proxy Blind Signature Scheme with Forward Security 计算机科学, 2021, 48(6A): 529-532. https://doi.org/10.11896/jsjkx.200700049 |
| [6] | 叶胜男, 陈建华. 一个强安全的无证书签名方案的分析和改进 Security Analysis and Improvement of Strongly Secure Certificateless Digital Signature Scheme 计算机科学, 2021, 48(10): 272-277. https://doi.org/10.11896/jsjkx.201200117 |
| [7] | 蒲泓全, 崔喆, 刘霆, 饶金涛. 安全性电子投票方案研究综述 Comprehensive Review of Secure Electronic Voting Schemes 计算机科学, 2020, 47(9): 275-282. https://doi.org/10.11896/jsjkx.190900125 |
| [8] | 董奇颖, 单轩, 贾春福. 口令Zipf分布对相关安全协议的影响分析 Impact of Zipf's Law on Password-related Security Protocols 计算机科学, 2020, 47(11): 42-47. https://doi.org/10.11896/jsjkx.200500144 |
| [9] | 蔡泳, 钱俊彦, 潘海玉. 基于度量线性时态逻辑的近似安全性 Approximate Safety Properties in Metric Linear Temporal Logic 计算机科学, 2020, 47(10): 309-314. https://doi.org/10.11896/jsjkx.191000175 |
| [10] | 孙宝华, 胡楠, 李东洋. 基于神经网络和NLP的软件需求安全分析研究 Analysis Research of Software Requirement Safety Based on Neural Network and NLP 计算机科学, 2019, 46(6A): 348-352. |
| [11] | 曹义亲, 曹婷, 黄晓生. 基于àtrous-NSCT变换和区域特性的图像融合方法 Image Fusion Method Based on àtrous-NSCT Transform and Region Characteristic 计算机科学, 2019, 46(6): 270-276. https://doi.org/10.11896/j.issn.1002-137X.2019.06.040 |
| [12] | 席新星, 罗晓清, 张战成. 基于3-D剪切波和广义高斯模型的多模态医学序列图像融合 Multi-modal Medical Volumetric Image Fusion Based on 3-D Shearlet Transform and Generalized Gaussian Model 计算机科学, 2019, 46(5): 254-259. https://doi.org/10.11896/j.issn.1002-137X.2019.05.039 |
| [13] | 徐丙凤, 何高峰, 张黎宁. 基于状态事件故障树的信息物理融合系统风险建模 Risk Modeling for Cyber-physical Systems Based on State/Event Fault Trees 计算机科学, 2019, 46(5): 105-110. https://doi.org/10.11896/j.issn.1002-137X.2019.05.016 |
| [14] | 罗旭东, 黄俏娟, 詹捷宇. 自动谈判及其基于模糊集的模型综述 A Survey of Automated Negotiation and Its Fuzzy Set Based Models 计算机科学, 2019, 46(12): 220-230. https://doi.org/10.11896/jsjkx.190800129 |
| [15] | 韦性佳,张京花,刘增芳,芦殿军. 具有前向安全性质的基于身份的聚合签名方案 Identity Based Aggregate Signature Scheme with Forward Security 计算机科学, 2018, 45(6A): 387-391. |
|
||
首页