Name
Abstract | ||
|---|---|---|
Abstract: Combining discrete state-machines with continuous behavior, hybrid systems are a well-established mathematical model for discrete systems acting in a continuous environment. As a priori infinite state systems, their computational properties are undecidable in the general model and the main line of research concentrates on model checking of finite abstractions of restricted subclasses of the general model. In our work, we use deductive methods, falling back upon the general-purpose theorem prover PVS. To do so we extend the classical approach for the verification of state-based programs by developing an inductive proof method to deal with the parallel composition of hybrid systems. It covers shared variable communication, label-synchronization, and especially the common continuous activities in the parallel composition of hybrid automata. Besides hybrid systems and their parallel composition, we formalized their operational step semantics and a number of proof-rules within PVS, for one of which we give also a rigorous completeness proof. Moreover, the theory is applied to the verification of a number of examples. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1109/ICECCS.2001.930163 | ICECCS |
Keywords | Field | DocType |
automatic control,discrete system,software systems,mathematical model,application software,automata theory,hybrid system,automata,embedded software,embedded system,state machine,theorem prover,synchronisation,hybrid systems,model checking,theorem proving | Automata theory,Model checking,Programming language,Computer science,Automated theorem proving,Automaton,Software system,Theoretical computer science,Hybrid system,Completeness (statistics),Undecidable problem | Conference |
Citations | PageRank | References |
12 | 0.81 | 16 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erika Ábrahám-Mumm | 1 | 59 | 4.55 |
| Martin Steffen | 2 | 12 | 0.81 |
| Ulrich Hannemann | 3 | 72 | 7.64 |