Formal Verification of Embedded Real-Time Software in Component-Based Application Frameworks

Pao-Ann Hsiung, Win-Bin See, Trong-Yen Lee, Jih-Ming Fu, and Sao-Jie Chen
Department of Computer Science and Information Engineering
National Chung Cheng University, Chiayi-621, Taiwan.
(In Proceedings of the 8th Asia-Pacific Software Engineering Conference (APSEC'01) IEEE Computer Society Press, December 2001.)


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.