计算机科学 ›› 2017, Vol. 44 ›› Issue (7): 128-136.doi: 10.11896/j.issn.1002-137X.2017.07.024
何云,王炜,李彤
HE Yun, WANG Wei and LI Tong
摘要： 软件系统的活性和安全性是判断软件可演化性的重要依据之一。现有方法多使用经典逻辑对系统的活性和安全性进行刻画。环境及涉众的复杂性使得软件的可演化性分析可能出现矛盾的输入。经典逻辑的无矛盾律导致其不能对软件系统的演化特性进行有效建模。针对该问题,提出了一种形式化的软件可演化性特征描述方法,该方法允许矛盾性输入的存在,可用于对软件可演化性等存在矛盾特性的系统进行建模和分析。该方法使用多值时序逻辑刻画软件系统的演化需求,同时提出了一种抽象软件模型对软件系统进行建模,通过抽象软件模型的活性和安全性来对软件系统的可演化特征进行描述。
| [1] LAMPORT L.Proving the correctness of multiprocess pro-grams[J].IEEE Transactions on Software Engineering,1977,SE-3(2):125-143. [2] WANG S Q,HUANG Z Q,HUANG C L,et al.Method Based on State/Even Fault Tree for Safety Analysis of Software[J].Journal of Chinese Computer Systems,2016,37(1):12-17.(in Chinese) 王思琪,黄志球,黄传林,等.一种基于状态事件故障树的软件安全性分析方法研究[J].小型微型计算机系统,2016,37(1):12-17. [3] SKELIN M,WOGNSEN E R,OLESEN M C,et al.Model checking of finite-state machine-based scenario-aware dataflow using timed automata[C]∥10th IEEE International Symposium on Industrial Embedded Systems(SIES),2015.Piscataway,NJ:IEEE,2015:1-10. [4] BELLI F,BEYAZLT M,ENDO A T,et al.Fault domain-based testing in imperfect situations:a heuristic approach and case studies[J].Software Quality Control,2015,23(3):423-452. [5] UZAM M,LI Z,ZHOU M C.Identification and elimination of redundant control places in petri net based liveness enforcing supervisors of FMS[J].International Journal of Advanced Manufacturing Technology,2007,35(1):150-168. [6] BOUDI Z,KOURSI E,COLLART-DUTILLEUL S.Colored Pe-tri Nets formal transformation to B machines for safety critical software development[C]∥International Conference on Industrial Engineering and Systems Management,2015.Piscataway,NJ:IEEE,2015:12-18. [7] WANG X B,DUAN Z H.Model Checking for Temporal Logic Programs[J].Computer Science,2009,6(10):164-167.(in Chinese) 王小兵,段振华.时序逻辑程序的模型检测[J].计算机科学,2009,6(10):164-167. [8] XU C,LIU J F,SUN J G.Security Protocol Model Checking Based on Classcial Logic[J].Computer Science,2008,35(6):20-24.(in Chinese) 徐畅,刘吉锋,孙吉贵.基于经典逻辑的安全协议模型检测方法[J].计算机科学,2008,35(6):20-24. [9] PNUELI A.The temporal logic of programs[C]∥18th Annual Symposium on Foundations of Computer Science,1977.Piscata-way,NJ:IEEE,1977:46-57. [10] EMERSON E A,HALPERN J Y.Sometimes and not never revisited:on branching versus linear time temporal logic[J].Journal of the ACM,1986,33(1):151-178. [11] QIAN J Y,XU B W.Model Checking CTL Based on Complete Abstraction Interpretation[J].Chinese Journal of Computers,2009,32(5):992-1001.(in Chinese) 钱俊彦,徐宝文.基于完备抽象解释的模型检验CTL公式研究[J].计算机学报,2009,32(5):992-1001. [12] KRIPKE S.Semantic considerations on modal logic[J].Acta Philosophica Fennica,1963(16):83-94. |
| No related articles found! |
|
||
首页