Computer Science ›› 2017, Vol. 44 ›› Issue (7): 128-136.doi: 10.11896/j.issn.1002-137X.2017.07.024

Previous Articles     Next Articles

Formal Method for Describing Software Evolution Ability Feature

HE Yun, WANG Wei and LI Tong   

  • Online:2018-11-13 Published:2018-11-13

Abstract: The liveness and safety are the most important basis for judging software systems evolution ability.The exi-sting modeling methods use classical logic to describe the liveness and safety of systems.The complexity of the environment and stakeholders leads to conflicting input when analyzing software evolution ability.Because of the non-contradiction law,classical logic can’t model the software system evolution ability effectively.Aiming at this problem,a formal method for describing the software evolution ability was proposed.The method allows contradictions,and can be used for modeling and analyzing systems with contradictions such as software evolution ability.The method uses multi-value temporal logic to describe software system evolution requirements,and proposes a software abstraction model to model software system.It can describe software system evolution ability by analyzing SAM’s liveness and safety.

Key words: Liveness,Safety,Contradiction,Software evolution ability,Multi-value temporal logic

[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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!