Name
Title | ||
|---|---|---|
Formal Verification of Embedded Real-Time Software in Component-Based Application Frameworks |
Abstract | ||
|---|---|---|
Producing correct software is a premier goal or applicationframeworks that are targeted at Embedded Real-Time Systems because incorrect software are not only of nouse but might also cause severe system damage.It is shownhow formal verification can be elegantly, seamlessly, andscalably integrated into a component-based object-orientedapplication 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 ) theexecution 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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1109/APSEC.2001.991461 | APSEC |
Keywords | Field | DocType |
common system model,formal synthesis,model checker,model checking,incorrect software,embedded real-time software,component-based object-orientedapplication framework,compositional software verification framework,vertaf application framework,real-time software,component-based application frameworks,producing correct software,formal verification,embedded systems,object oriented programming,object oriented,real time,software verification,system modeling | Programming language,Model checking,Object-oriented programming,Systems engineering,Computer science,Real-time computing,Software,Formal methods,Software verification and validation,System model,Software verification,Formal verification | Conference |
Citations | PageRank | References |
5 | 0.47 | 18 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pao-ann Hsiung | 1 | 624 | 68.75 |
| winbin see | 2 | 30 | 3.19 |
| Trong-yen Lee | 3 | 98 | 20.70 |
| Jih-ming Fu | 4 | 33 | 3.16 |
| Sao-Jie Chen | 5 | 523 | 62.97 |