Model-based analysis of distributed real-time embedded system composition

Key challenges in distributed real-time embedded (DRE) system developments include safe composition of system components and mapping the functional specifications onto the target platform. Model-based verification techniques provide a way for the design-time analysis of DRE systems enabling rapid evaluation of design alternatives with respect to given performance measures before committing to a specific platform. This paper introduces a semantic domain for model-based analysis of a general class of DRE systems capturing their key time-based performance measures. We then utilize this semantic domain to develop a verification strategy for preemptive schedulability using available model checking tools. The proposed framework and verification strategy is demonstrated on a mission-critical avionics DRE system case study. Categories and Subject Descriptors I.6.4 [Simulation and Modeling]: Model Validation and Analysis General Terms design, verification

• Type: Conference
• Year: 2005
• Where: EMSOFT
• Authors: Gabor Madl, Sherif Abdelwahed
• Keywords: DRE Systems, EMSOFT 2005, Performance Measures, Semantic Domain