A survey of formal verification methods and tools for embedded and real-time systems

被引:4
作者
Cheng, Albert Mo Kim [1 ]
机构
[1] Univ Houston, Real Time Syst Lab, Dept Comp Sci, Houston, TX 77204 USA
基金
美国国家科学基金会;
关键词
verification; formal methods; real-time systems; embedded systems; specification; analysis; software engineering; system design;
D O I
10.1504/IJES.2006.014854
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
To facilitate the control of increasingly complex physical systems such as drive-by-wire automobiles and fly-by-wire airplanes, embedded and networked computer systems with numerous hardware and software components are increasingly required. However, this complexity also leads to more potential errors and faults, during both the design/implementation phase and the deployment/runtime phase. It is therefore essential to verify the system under control as well as the control system itself with the aid of mechanical verification tools. This paper surveys verification techniques using model checking, Statechart/Statemate, timed automata, timed Petri nets, timed process algebra, real-time logic and semantic rule-based analysis.
引用
收藏
页码:184 / 195
页数:12
相关论文
共 93 条
[91]   Optimization of rule-based systems using state space graphs [J].
Zupan, B ;
Cheng, AMK .
IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 1998, 10 (02) :238-254
[92]  
Zupan B., 1995, P IFAC C ART INT REA
[93]  
[No title captured]