Modeling and verification of de-icing software safety requirement based on expanded Petri net

[1] Leveson N G.Software safety:why,what,and how [J].ACM Computing Surveys,1986,18(2):125-163 [2] 刘克,单志广,王戟,等."可信软件基础研究"重大研究计划综述[J].中国科学基金,2008(3):145-151Liu Ke,Shan Zhiguang,Wang Ji,et al.Overview on major research plan of trustworthy software[J].Science Foundation in China,2008(3):145-151(in Chinese) [3] 袁崇义.Petri网原理与应用[M].北京:电子工业出版社,2005:51-75Yuan Chongyi.The principle and application of Petri net[M].Beijing: Electronics Industry Press,2005:51-75(in Chinese) [4] 姚洪英,范铁生,苏红丽,等.基于Petri网的分布式实时多媒体同步模型[J].沈阳工业大学学报,2004,26(1):96-98Yao Hongying,Fan Tiesheng,Su Hongli,et al.A distributed realtime multimedia synchronic model based on Petri net[J].Journal of Shenyang University of Technolgy,2004,26(1):96-98(in Chinese) [5] Cicirelli F,Furfaro A,Nigro L.An approach to protocol modeling and validation[C]//39th Annual Simulation Symposium.CA:IEEE Computer Society,2006:1-8 [6] Franck C,Olivier H R.Structural translation from time Petri nets to timed automata[J].Journal of Systems and Software,2006,79(10):1456-1468 [7] Bell D G,Brat G P.Automated software verification & validation: an emerging approach for ground operations[C]//Aerospace Conference,2008 IEEE.NY:IEEE Press,2008:1-8 [8] Heitmeyer C L,Archer M M,Leonard E I.Applying formal methods to a certifiably Secure software system[J].Software Engineering,IEEE Transactions on, 2008,34(1):82-98 [9] Li Zhen,Liu Bin,Ma Ning,et al.Formal testing applied in embedded software[C]//8th International Conference on Reliability,Maintainability and Safety.Washington,DC:IEEE Computer Society,2009,2:1-5 [10] Ma Ning,Bao Xiaohong,Li Zhen,et al.Verification of safety-critical software requirement based on Petri-net model checking[C]//Supplemental Proceedings 20th International Symposium on Software Reliability Engineering.Washington,DC:IEEE Computer Society,2009 [11] 李震,刘斌,殷永峰,等.基于扩展Petri网的安全关键软件需求模型检验[J].沈阳工业大学学报,2011,33(1):113-120Li Zhen,Liu Bin,Yin Yongfeng,et al.Requirement model checking of safety-critical software based on expanded Petri net [J].Journal of Shenyang University of Technology,2011,33(1):113-120(in Chinese) [12] 古天龙.软件开发的形式化方法[M].1版.北京: 高等教育出版社,2005:47-51Gu Tianlong.Formal methods of software development[M].1st ed.Beijing:Higher Education Press,2005:47-51(in Chinese) [13] 沈胜宇.模型检验的反例解释[D].长沙: 国防科学技术大学计算机学院,2005:1-7Shen Shengyu.Explaining counterexample of model checking[D].Changsha:School of Computer,National University of Defense Technology,2005:1-7(in Chinese) [14] Roberto C,Alessandro C,Charles A J,et al.NuSMV 2.4 user manual[EB/OL].Italy,Trento: CMU and ITC-irst,2005[2009].http://nusmv.irst.itc.it/