Language For Unified Verification And Implementation For Distributed Avionics

In designing, verifying, and validating distributed systems today, an engineer is often faced with having to specify a system multiple times. For example, the engineer might specify it once in a model-checker for formal analysis, in an architectural description language for requirements analysis, and in a programming language for testing. By specifying the same system multiple times, there is risk that each specification has different semantics, so that the system tested differs from the one verified, for example. To help solve this problem, we envision an architectural domain-specific language (ADSL), or a unified language from which formal models, executable code, and architectural models can be synthesized. To make our problem tractable, we focus on distributed fault-tolerant systems. We present the Language for Integrated Modeling and Analysis (LIMA), a particular ADSL that we have designed. We describe LIMA and its application to case studies motivated by avionics design.