计算机科学 ›› 2020, Vol. 47 ›› Issue (10): 309-314.doi: 10.11896/jsjkx.191000175
蔡泳, 钱俊彦, 潘海玉
CAI Yong, QIAN Jun-yan, PAN Hai-yu
摘要： 近年来,计算机系统的定量验证已经引起了学术界和工业界足够的关注,其中取值于度量空间的系统性质研究为定量验证的发展开辟了一条新途径。在系统验证中常用线性时间属性来刻画系统的性质,而安全性作为线性时间属性中一类至关重要的基础属性,能保证系统在运行过程中不会发生“坏”的事情,其在度量背景下的推广形式也应该得到关注。为此,文中研究伪超度量空间上安全性的扩展问题,首先对已有的度量线性时态逻辑进行适当的补充,使其能充分地刻画度量背景下的线性时间属性;然后引入距离阈值α,提出一种α-安全性的概念,从而将经典的安全性提升到伪超度量空间上;最后讨论度量线性时态逻辑与α-安全性之间的关系。这些结论为取值于度量空间的系统的安全性验证提供了理论依据。
中图分类号:
| [1] BAIER C,KATOEN J P.Principles of model checking[M].The MIT Press,2008. [2] MANNA Z,PNUELI A.The temporal logic of reactive and concurrent systems:Specification [M].Springer-verlag,1992. [3] LIN H M,ZHANG W H.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912. [4] WANG X B,DUAN Z H.Model checking for temporal logicprograms[J].Computer Science,2009,36(10):164-167. [5] WANG Z Z.Survey of model checking[J].Computer Science,2013,40(6A):1-14. [6] HOU G,ZHOU K J,YONG J W,et al.Survey of state explosion problem in model checking [J].Computer Science,2013,40(6A):77-86. [7] ZHU C Y,CHANG L,XU Z B,et al.Model checking of temporal description logic ALC-LTL based on label Büchi automata[J].Computer Science,2013,40(10):166-171. [8] BU L,XIE D B.Formal verification of Hybrid system[J].Journal of Software,2014,25(2):219-233. [9] WANG J,ZHAN N J,FENG X Y,et al.Over-view of formalmethods[J].Journal of Software,2019,30(1):33-61. [10]ALPERN B,SCHNEIDER F B.Defining liveness[J].Information Processing Letters,1985,21(4):181-185. [11]ALPERN B,SCHNEIDER F B.Recognizing safety and liveness[J].Distributed Computing,1987,2(3):117-126. [12]KUPFERMAN O,VARDI M Y.Model checking of safetyproperties[J].Formal Methods in System Design,2001,19(3):291-314. [13]FARAN R,KUPFERMAN O.Spanning the spectrum fromsafety to liveness[J].Acta Informatica,2018,55(8):703-732. [14]KUPFERMAN O,VARDI G.On relative and probabilistic finite counterability[J].Formal Methods in System Design,2018,52(2):117-146. [15]SISTLA A P.Safety,liveness and fairness in temporal logic[J].Formal Aspects of Computing,1994,6(5):495-511. [16]LI Y M,DROSTE M,LEI L H.Model checking of linear-time properties in multi-valued systems[J].Information Sciences,2017,377:51-74. [17]LI Y M.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2017,320:17-39. [18]KATOEN J P,LEI S,ZHANG L.Probably safe or live[C]//Eacsl Conference on Computer Science Logic.2014:1-10. [19]FAHRENBERG U,LARSEN K G,THRANE C R.A quantitative characterization of weighted Kripke structures in temporal logic [C]//Doctoral Workshop on Mathematical & Engineering Methods in Computer Science.DBLP,2009. [20]PAN H Y.Lattice-valued quantitative verification of state transition systems[D].Shanghai:East China Normal University,2012. [21]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. [22]PAN H Y,LI Y M,CAO Y Z,et al.Model checking computation tree logic over finite lattices[J].Theoretical Computer Scien-ce,2016,612(C):45-62. [23]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. [24]LIANG C J,LI Y M.The model checking problem of computing tree logic based on generalized possibility measures[J].Acta Electronica Sinica,2017,45(11):2641-2648. [25]FAN Y H,LI Y M.The realizability of fuzzy linear temporal logic[J].Acta Electronica Sinica,2018,46(2):341-346. [26]FAN Y H,LI Y M,PAN H Y.Computation tree logic model checking for nondeterminisitc fuzzy Kripke structure[J].Acta Electronica Sinica,2018,46(1):152-159. [27]LEI L H,WANG J.Parallelization of LTL model checking based on possibility measure [J].Computer Science,2018,45(4):71-75. [28]ZHU Y,YUAN H J,QIAN J Y,et al.Some notes on fuzzy alternating-time temporal logic [J].Journal of Frontiers of Computer Science and Technology,2018,12(12):2033-2040. [29]ALFARO L D,FAELLA M,STOELINGA M.Linear andbranching system metrics[J].IEEE Transactions on Software Engineering,2009,35(2):258-273. [30]CAO Y Z,SUN S X,WANG H Q,et al.A behavioral distance for fuzzy-transition sys-tems[J].IEEE Transactions on Fuzzy Systems,2013,21(4):735-747. [31]BU T M,WU H Y,CHEN Y X.Computing behavioural distance for fuzzy transition systems[C]//International Symposiumon Theoretical Aspects of Software Engineering.IEEE Computer Society,2017. [32]CHEN T L,HAN T T,CAO Y Z.Polynomial-time algorithms for computing distances of fuzzy transition systems[J].Theore-tical Computer Science,2018,727:24-36. |
| [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] | 石铁柱, 钱俊彦, 潘海玉. 模糊安全性和活性 Fuzzy Safety and Liveness Properties 计算机科学, 2021, 48(4): 31-36. https://doi.org/10.11896/jsjkx.200500036 |
| [7] | 冉丹, 陈哲, 孙毅, 杨志斌. 基于程序转化的SCADE模型检测 SCADE Model Checking Based on Program Transformation 计算机科学, 2021, 48(12): 125-130. https://doi.org/10.11896/jsjkx.201100080 |
| [8] | 叶胜男, 陈建华. 一个强安全的无证书签名方案的分析和改进 Security Analysis and Improvement of Strongly Secure Certificateless Digital Signature Scheme 计算机科学, 2021, 48(10): 272-277. https://doi.org/10.11896/jsjkx.201200117 |
| [9] | 蒲泓全, 崔喆, 刘霆, 饶金涛. 安全性电子投票方案研究综述 Comprehensive Review of Secure Electronic Voting Schemes 计算机科学, 2020, 47(9): 275-282. https://doi.org/10.11896/jsjkx.190900125 |
| [10] | 董奇颖, 单轩, 贾春福. 口令Zipf分布对相关安全协议的影响分析 Impact of Zipf's Law on Password-related Security Protocols 计算机科学, 2020, 47(11): 42-47. https://doi.org/10.11896/jsjkx.200500144 |
| [11] | 夏奴奴, 杨晋吉, 赵淦森, 莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证 Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model 计算机科学, 2019, 46(8): 206-211. https://doi.org/10.11896/j.issn.1002-137X.2019.08.034 |
| [12] | 孙宝华, 胡楠, 李东洋. 基于神经网络和NLP的软件需求安全分析研究 Analysis Research of Software Requirement Safety Based on Neural Network and NLP 计算机科学, 2019, 46(6A): 348-352. |
| [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] | 韩英杰, 周清雷, 朱维军. 基于DNA计算的计算树逻辑模型检测方法研究进展 Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking 计算机科学, 2019, 46(11): 25-31. https://doi.org/10.11896/jsjkx.181102091 |
| [15] | 周女琪, 周宇. 基于概率模型检测的Web服务组合多目标验证 Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking 计算机科学, 2018, 45(8): 288-294. https://doi.org/10.11896/j.issn.1002-137X.2018.08.052 |
|
||
首页