Producing correct software is a premier goal for
application frameworks that are targeted at Embedded
Real-Time Systems because incorrect software are not only of no
use but might 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 a 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.