Towards modularized verification of distributed time-triggered systems

The correctness of a system according to a given specification is essential, especially for safety-critical applications. One such typical application domain is the automotive sector, where more and more safety-critical functions are performed by largely software-based systems. Verification techniques can guarantee correctness of the system. Although automotive systems are relatively small compared to other systems (e.g. business information systems) they are still too large for monolithic verification of the system as a whole. Tackling this problem, we present an approach for modularized verification, aiming at time-triggered automotive systems. We show how the concept of tasks, as used in current automotive operating systems, can be modeled in a CASE tool, verified and deployed. This results in a development process facilitating verification of safety-critical, real-time systems at affordable cost.