This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05)
Model-Checking of Component-Based Event-Driven Real-Time Embedded Software
Seattle, Washington
May 18-May 20
ISBN: 0-7695-2356-0
Zonghua Gu, University of Virginia, Charlottesville, VA
Kang G. Shin, University of Michigan, Ann Arbor, MI
As complexity of real-time embedded software grows, it is desirable to use formal verification techniques to achieve a high level of assurance. We discuss application of model-checking to verify system-level concurrency properties of component-based real-time embedded software based on CORBA Event Service, using Avionics Mission Computing software as an application example. We use the process algebra FSP to formalize specification of software components and system architecture, previously only available in the form of natural language and prone to misinterpretation and misunderstanding, and use model-checking to verify system-level concurrency properties. We also discuss effective techniques for coping with the state-space explosion problem by exploiting application domain semantics. We have applied our analysis techniques to realistic application scenarios provided by our industry partner to demonstrate their utility and power.
Citation:
Zonghua Gu, Kang G. Shin, "Model-Checking of Component-Based Event-Driven Real-Time Embedded Software," isorc, pp.410-417, Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.