Name
Abstract | ||
|---|---|---|
We present a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as Hybrid Automata驴communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure, and temperature. The system requirements are specified in a temporal logic with stop watches, and verified by symbolic fixpoint computation. The verification procedure驴implemented in the Cornell Hybrid Technology Tool, HYTECH驴applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded, and duration requirements of digital controllers, schedulers, and distributed algorithms. |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1109/32.489079 | Software Engineering, IEEE Transactions |
Keywords | Field | DocType |
automata theory,mathematica,finite state machines,distributed algorithms,finite control,pressure,variable derivatives,real-time temporal logic,time-bounded,continuous environment parameters,duration requirements,automatic symbolic verification,algebraic specification,continuous dynamics,model-checking procedure,symbol manipulation,temperature,liveness,automatic verification,hytech,software tools,schedulers,model checking procedure,safety checking,real-valued variables,duration properties,hybrid technology tool,symbolic verification,time-bounded requirements,temporal logic,digital controllers,communicating machines,hybrid automata,time,embedded systems,safety,stop-watches,symbolic computation,real-time systems,formal specification,formal verification,symbolic fixpoint computation,linear constraints,technical report,symbolic analysis,digital control,temperature control,logic,model checking,automatic control,embedded system,computer science,real time systems,automata,control systems | Model checking,Computer science,Symbolic computation,Real-time computing,Theoretical computer science,Finite-state machine,Symbolic data analysis,Temporal logic,Hybrid system,Embedded system,Formal verification,Liveness | Journal |
Volume | Issue | ISSN |
22 | 3 | 0098-5589 |
ISBN | Citations | PageRank |
0-8186-4480-X | 295 | 39.16 |
References | Authors | |
37 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rajeev Alur | 1 | 17253 | 1413.65 |
| Thomas A. Henzinger | 2 | 361 | 43.06 |
| Pei-hsin Ho | 3 | 2577 | 305.29 |