Formal verification of embedded real-time software in component-based application frameworks

Producing correct software is a major goal for application frameworks that are targeted at embedded real-time systems because incorrect software is of no use and may also cause severe system damage. It is shown how formal verification can be elegantly, seamlessly, and scalably integrated into a component-based object-oriented application framework for embedded real-time systems. Two issues in such technology integration are addressed: (1) the choice of a common system model, and (2) the integration of formal synthesis and model checking. Solutions are provided, respectively, in the form of (1) proposing a new formal object-oriented model (FOOM), and (2) the execution of model checkers within synthesis algorithms. Technically, we propose a compositional software verification framework, in which model checking is employed, with state-space reduction techniques adapted for embedded real-time software. A separate verifier component is proposed for modular integration as illustrated by its implementation in the VERTAF application framework. An example illustrates the success of our approach and the benefits gained through integrating formal verification.