Name
Abstract | ||
|---|---|---|
Hybrid systems are a well-established mathematical model for embedded systems. Such systems, which combine discrete and continuous behavior, are increasingly used in safety-critical applications. To guarantee safe functioning, formal verification techniques are crucial. While research in this area concentrates on model checking, deductive techniques attracted less attention. In this paper we use the general purpose theorem prover PVS for the rigorous formalization and analysis of hybrid systems. To allow for machine-assisted proofs, we implement a deductive assertional proof method within PVS. The sound and complete proof system allows modular proofs in that it comprises a proof rule for the parallel composition. Besides hybrid systems and the proof system, a number of examples are formalized within PVS. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-45654-6_8 | EUROCAST |
Keywords | Field | DocType |
hybrid systems,hybrid system,assertion-based analysis,model checking,proof rule,complete proof system,modular proof,deductive assertional proof method,machine-assisted proof,deductive technique,proof system,embedded system,mathematical model,theorem prover,formal verification | Specification language,Model checking,Computer science,Automated theorem proving,Theoretical computer science,Mathematical proof,Modular design,Hybrid system,Formal verification,Proof assistant | Conference |
Volume | ISSN | ISBN |
2178 | 0302-9743 | 3-540-42959-X |
Citations | PageRank | References |
3 | 0.42 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erika Ábrahám-Mumm | 1 | 59 | 4.55 |
| Ulrich Hannemann | 2 | 72 | 7.64 |
| Martin Steffen | 3 | 122 | 10.32 |