| Abstract |
|
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.
|
 Additional Information
|
Citation:
Pao-Ann Hsiung, Win-Bin See, Trong-Yen Lee, Jih-Ming Fu, Sao-Jie Chen,
"Formal Verification of Embedded Real-Time Software in Component-Based Application Frameworks,"
apsec,
p. 71,
Eighth Asia-Pacific Software Engineering Conference (APSEC'01),
2001
|
