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

Authors: Albert Mo Kim Cheng

Addresses: Department of Computer Science, Real-Time Systems Laboratory, University of Houston, Houston, TX 77204-3010, USA

Abstract: 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.

Keywords: verification; formal methods; real-time systems; embedded systems; specification; analysis; software engineering; system design; drive-by-wire automobiles; fly-by-wire airplanes.

DOI: 10.1504/IJES.2006.014854

International Journal of Embedded Systems, 2006 Vol.2 No.3/4, pp.184 - 195

Published online: 12 Aug 2007 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article