Model-Based Analysis and Formal Verification of Component-Based Real-Time Embedded Software

As the complexity of modern real-time embedded systems grows, it is important to perform analysis of system properties at early design stages, in order to help the designer make high-level design decisions that have a large impact on the overall system. This paper presents a set of techniques and tools for model-based analysis and formal verification of component-based real-time embedded software, with Avionics Mission Computing (AMC) as an example application domain. Domain-specific models are used to capture all aspects of a real-time embedded system, including software components and architecture, timing and resource constraints, processes and threads, execution platforms, etc. We first discuss model-level static analysis techniques, including dependency analysis, execution rate assignment, worst-case execution time/schedulability analysis, and automated component allocation. We then discuss application of model-checking to verify system-level concurrency properties, by using 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. We also discuss effective techniques for improving model-checking scalability. These analysis techniques are applied to real-world application scenarios provided by our industr