An Analysis on Formal Models of Computation for the Avionics Systems Domain

Cyber-physical systems (CPS) and embedded systems have a large application domain, from simple consumer electronics products to complex systems with restricted safety requirements, such as avionics systems. As broadly known in the case of avionics systems, the occurrence of a failure can cause disastrous consequences. In this sense, the design of complex CPS can be made by using a formal approach, based on models of computation. Model of computation (MoC) is a set of rules that describe the semantics of both execution and concurrency in heterogeneous computational systems. MoCs can be categorized as timed or untimed. As an example, the synchronous (SY) model of computation is a timed MoC, whereas the synchronous dataflow (SDF) and the scenario-aware dataflow (SADF) are untimed. Yet, there are some gaps to fill in this context. For example, which is the MoC which better describes the application-specific requirements at a high level of abstraction while also being able to reach a feasible platform model implementation with required performance, and most importantly, without losing the characteristics and properties of the application domain. In this paper, we perform an analysis of the most commons models of computation (e.g., SY, SDF, and SADF) and demonstrate which one better fits the avionics systems domain, while at the same time being capable to provide a safe implementation of future digital avionics systems.