Producing correct software is a premier goal or 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 or 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 o our approach and the benefits gained through integrating formal verification.