ABSTRACT Techniques and Tools for Model-Based Design and Analysis of Embedded Real-Time Software by

As Embedded Real-Time (ERT) systems become more complex and safety-critical, there is a trend to raise software development level of abstraction from programming lan-guages to models. We have developed a suite of techniques and tools to improve industry acceptance of model-driven development of ERT software. As a result of collaboration among multiple institutions, an end-to-end tool-chain has been developed for the design and analysis of ERT software, with Avionics Mission Com-puting (AMC) as the main target application. As part of the tool-chain, we have developed a tool called AIRES for model-level static analysis. Compared to traditional static analy-sis techniques that work at the level of programming languages, AIRES works at a higher level of abstraction, and provides valuable dependency and timing information to the en-gineer at an early stage of the design cycle. AIRES mainly focuses on the static structural aspects while largely ignoring the dy-namic behavior of component interactions. We use model-checking to formalize the natural language description of the dynamic behavior of the AMC software, and verify safety and liveness properties. We also present several techniques to improve scalabilit