Combination of Model Checking and Theorem Proving to Verify Embedded Software

Combination of Model Checking and Theorem Proving to Verify Embedded Software

导出

摘要 In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software. In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software.

作者 XIAO Jian-yu, ZHANG De-yun, DONG Hao, CHEN Hai-quan 1. School of Electronics and Information Engineering, Xi’an Jiaotong University, Xi’an 710049, P.R. China 2. Institute of Laser and Information, Shaoyang University, Shaoyang 422000, P.R. China

出处《The Journal of China Universities of Posts and Telecommunications》 EI CSCD 2005年第4期80-84,87,共6页 中国邮电高校学报（英文版）

基金 This workis Supported by the National High-Technology Research and Development Program(863-301-05-03) .

关键词 model checking theorem proving high trustworthy software software verification model checking theorem proving high trustworthy software software verification

分类号 TP311.5 [自动化与计算机技术—计算机软件与理论]

引文网络
相关文献

参考文献15

1SINGHAL M.Research in high-confidence distributed information[A].Proceedings of IEEE Computer Society 20th Symposium on Reliable Distributed Systems[C].New Orleans(LA,USA),2001.Los Alamitos(CA,USA):IEEE Computer Society,2001.76-79.
2JOHNSON S D.Formal methods in embedded design[J].Computer,2003,36(11):104-106.
3BASTANI F B.High-Quality Customizable Embedded Software from COTS Components[A].Proceedings of IEEE Computer Society 20th Symposium on Reliable Distributed Systems[C].New Orleans(LA,USA),2001.Los Alamitos(CA,USA):IEEE Computer Society,2001.174-175.
4HEIMDAHL M P,HEITMEYER C L.Formal methods for developing high assurance computer systems:Working group report[A].Proceedings of Second IEEE Workshop on Industrial-Strength Formal Techniques(WIFT'98)[C].Boca Raton(FL,USA),1998.Piscataway(NJ,USA):IEEE,1998.1-60.
5CLARKE E,GRUMBERG O,PELED D.Model Checking[M].Cambridge(MA,USA):MIT Press,1999.
6ZHANG H.SATO:An efficient propositional prover[A].Proceedings of the International Conference on Automated Deduction(CADE'97)[C].Townsville(Australia),1997.New York(NY,USA):Springer-Verlag,1997.272-275.
7SHANKAR N.Combining theorem proving and model checking through symbolic analysis[A].Proceedings of 11th International Conference on Concurrency Theory,LNCS 1877[C].Philadelphia(PA,USA),2002.New York(NY,USA):Springer-Verlag,2002.1-16.
8MANNA Z,CHANG E,ANUCHITANUKUL A,et al.STeP:the Stanford Temporal Prover[R].STAN-CS-TR-03-1518,Stanford(CA,USA):Stanford University,2003.
9MIKHAILOV L,BUTLER M.An approach to combining B and Alloy[A].Proceedings of 2nd International Conference of B and Z Users(ZB'2002)[C].Grenoble(France),2002.New York(NY,USA):Springer-Verlag,2002.140-161.
10BEREZIN S.Model Checking and Theorem Proving:A Unified Framework[D].Pitsburgh(PA,USA):Carnegie Mellon University,2002.

1Lǔ Jian MA XiaoXing TAO XianPing CAO Chun HUANG Yu YU Ping.On environment-driven software model for Internetware[J].Science in China(Series F),2008,51(6):683-721. 被引量：17
2王磊.基于UML的模型软件开发应用与研究[J].计算机光盘软件与应用,2013,16(23):263-263.
3钟德明,刘斌,阮镰.嵌入式软件仿真测试单机平台实时任务调度方法研究[J].测控技术,2004,23(4):52-53.
4陈冬火,王林章,崔家林.Model Checking over Paraconsistent Temporal Logic[J].Journal of Donghua University(English Edition),2008,25(5):571-580.
5产品推荐[J].多媒体世界,2007(6):16-19.
6Joice Barbosa Mendes Alexandre Carlos Brandao Ramos.Software Model for a Computer Based Training for an HVDC Control Desk Simulator[J].通讯和计算机（中英文版）,2010,7(9):27-31.
7施冬梅.嵌入式软件动态测试数据采集的研究[J].绵阳师范学院学报,2010,29(8):102-105.
8Xie Xin Lu Dongxin Miao Jing Xu Lifeng (Chengdu Institute of ZTE Corporation,Chengdu 610041,China).Telecom-Oriented Embedded Software Support Platform[J].ZTE Communications,2004,2(1):18-21.
9Robert Murphy,Patrick Otoo Bobbie.Embedded Software Control of a Hybrid Vehicle＇s ECU/FCM System[J].Computer Technology and Application,2012,3(1):8-15.
10Haoxue Wang Ke Zhu Yuxiang Hu Dongnian Cheng.Trustworthy Mobile Network Architecture Based on Locator/Identity Split[J].Journal of Systems Science and Information,2008,6(1):71-80.

The Journal of China Universities of Posts and Telecommunications

2005年第4期

浏览历史

内容加载中请稍等...

Combination of Model Checking and Theorem Proving to Verify Embedded Software

参考文献15

相关作者

相关机构

相关主题

浏览历史