Automatic Symbolic Verification of Embedded Systems
| dc.contributor.author | Alur, Rajeev | en_US |
| dc.contributor.author | Henzinger, Thomas A. | en_US |
| dc.contributor.author | Ho, Pei-Hsin | en_US |
| dc.date.accessioned | 2007-04-23T18:02:14Z | |
| dc.date.available | 2007-04-23T18:02:14Z | |
| dc.date.issued | 1995-05 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 423557 bytes | |
| dc.format.extent | 548549 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1513 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/7170 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Automatic Symbolic Verification of Embedded Systems | en_US |
| dc.type | technical report | en_US |