Application Development for Safety Critical Distributed Embedded Systems with Model Verification

The increasing use of distributed applications in real-time and safety critical embedded systems results in the need for functional and non-functional system verification in the design process. This paper proposes model verification as solution to identify concept ional design failures in advance, and to verify model correctness in an abstract level.

With an extension to classical model checking environments like SPIN, or real-time model verification tools like UPPAAL, it is possible to analyze communication in distributed systems and verify design decisions compared to real hardware and system environments like network bandwidth or computing capabilities. With identification of communication points in distributed embedded systems and annotation of non-functional system requirements model verification can be adapted to support application development for safety critical systems in automotive or avionics.