A Theory for Event-Driven Specifications Using Focus and MontiArc on the Example of a Data Link Uplink Feed System

Abstract

The development of avionics message communication systems is expensive due to their complexity and the need to get them accepted by the certification authorities. We need to develop high-integrity software, but we also face cost pressure. For managing complex large systems, several time-synchronous modeling languages have been proposed. While these are appropriate for hardware specifications, when it comes to specifying distributed software systems, an event-based specification style is better suited. We present an event-based specification theory based on the framework Focus by giving the signatures and data types for specifications using event automata. For this, we capture message processing order as a further dimension of non-determinism by specifying a general timed merge component. These event automata can represent underspecification of behavior, and a refinement calculus can be applied to these for a stepwise reduction of non-determinism. Furthermore, we present the necessary concepts for enabling a user-friendly specification and simulation of event-based systems by using the architecture description language MontiArc. Finally, we evaluate our approach by performing a top-down architecture design of an avionics case study and demonstrating event-based specifications of requirements in MontiArc. The presented methodology improves the management of complexity, reduces costs, and increases the system quality.