Model-checking of component-based event-driven real-time embedded software

As complexity of real-time embedded software grows, it is de-sirable 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 ex-ample. 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 misinter-pretation and misunderstanding, and use model-checking to ver-ify system-level concurrency properties. We also discuss effec-tive 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. 1