A survey of formal verification methods and tools for embedded and real-time systems
by Albert Mo Kim Cheng
International Journal of Embedded Systems (IJES), Vol. 2, No. 3/4, 2006

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.

Online publication date: Sun, 12-Aug-2007

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Embedded Systems (IJES):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com