Modelling and verification of predictable data flow in real-time systems
MetadataShow full item record
As vehicle electronic control systems become responsible for an increasing number of functions, developers of such systems find themselves pulled in two directions: the need to perform more and more computation while at the same time reducing cost, weight and power consumption. Traditionally, safety isolation and fault containment of software tasks has been achieved through either physical or temporal segregation. This approach is reliable but inefficient in terms of processor utilization. Recently, there has been a move towards systems which achieve better processor utilization by executing all tasks together and guaranteeing safety isolation and fault containment by means of formal verification. First, a definition for one such system was developed, based on PharOS and Giotto. The system modelled attempts to ensure observably deterministic data flow (i.e., inputs from and outputs to other systems), but allows for non-observable nondeterminism. It also allows for sporadic deadline overruns and accounts for criticality during fault handling. Second, a method for verifying a given input system definition (system, set of tasks and fault model) for predictable data flow was developed. A stand-alone tool was made that performs this verification and displays the results graphically. The core exhaustive verification is performed by the Spin model checker.