Event Order Abstraction for Parametric Real-Time System Verification
We present a new abstraction technique, event order abstraction (EOA), for parametric safety verification of real-time systems in which ``correct orderings of events'' needed for system correctness are maintained by timing constraints on the systems' behavior. By using EOA, one can se...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
2008
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/41891 |
| _version_ | 1811081526045048832 |
|---|---|
| author | Umeno, Shinya |
| author2 | Nancy Lynch |
| author_facet | Nancy Lynch Umeno, Shinya |
| author_sort | Umeno, Shinya |
| collection | MIT |
| description | We present a new abstraction technique, event order abstraction (EOA), for parametric safety verification of real-time systems in which ``correct orderings of events'' needed for system correctness are maintained by timing constraints on the systems' behavior. By using EOA, one can separate the task of verifying a real-time system into two parts: 1. Safety property verification of the system given that only correct event orderings occur; and 2. Derivation of timing parameter constraints for correct orderings of events in the system.The user first identifies a candidate set of bad event orders.Then, by using ordinary untimed model-checking, the user examines whether a discretized system model in which all timing constraints are abstracted away satisfies a desirable safety property under the assumption that the identified bad event orders occur in no system execution. The user uses counterexamples obtained from the model-checker to identify additional bad event orders, and repeats the process until the model-checking succeeds. In this step, the user obtains a sufficient set of bad event orders that must be excluded by timing synthesis for system correctness.Next, the algorithm presented in the paper automatically derives a set of timing parameter constraints under which the system does not exhibit the identified bad event orderings. From this step combined with the untimed model-checking step,the user obtains a sufficient set of timing parameter constraints under which the system executes correctly with respect to a given safety property.We illustrate the use of EOA with a train-gate example inspired by the general railroad crossing problem. We also summarize three other case studies, a biphase mark protocol, the IEEE 1394 root contention protocol, and the Fischer mutual exclusion algorithm. |
| first_indexed | 2024-09-23T11:47:56Z |
| id | mit-1721.1/41891 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T11:47:56Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | mit-1721.1/418912019-04-12T09:43:47Z Event Order Abstraction for Parametric Real-Time System Verification Umeno, Shinya Nancy Lynch Theory of Computation parametric verification event-based approach counter-example guided abstraction refinement (CEGAR) automatic timing synthesis We present a new abstraction technique, event order abstraction (EOA), for parametric safety verification of real-time systems in which ``correct orderings of events'' needed for system correctness are maintained by timing constraints on the systems' behavior. By using EOA, one can separate the task of verifying a real-time system into two parts: 1. Safety property verification of the system given that only correct event orderings occur; and 2. Derivation of timing parameter constraints for correct orderings of events in the system.The user first identifies a candidate set of bad event orders.Then, by using ordinary untimed model-checking, the user examines whether a discretized system model in which all timing constraints are abstracted away satisfies a desirable safety property under the assumption that the identified bad event orders occur in no system execution. The user uses counterexamples obtained from the model-checker to identify additional bad event orders, and repeats the process until the model-checking succeeds. In this step, the user obtains a sufficient set of bad event orders that must be excluded by timing synthesis for system correctness.Next, the algorithm presented in the paper automatically derives a set of timing parameter constraints under which the system does not exhibit the identified bad event orderings. From this step combined with the untimed model-checking step,the user obtains a sufficient set of timing parameter constraints under which the system executes correctly with respect to a given safety property.We illustrate the use of EOA with a train-gate example inspired by the general railroad crossing problem. We also summarize three other case studies, a biphase mark protocol, the IEEE 1394 root contention protocol, and the Fischer mutual exclusion algorithm. 2008-07-28T13:30:25Z 2008-07-28T13:30:25Z 2008-07-28 MIT-CSAIL-TR-2008-048 http://hdl.handle.net/1721.1/41891 Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 19 p. application/pdf application/postscript |
| spellingShingle | parametric verification event-based approach counter-example guided abstraction refinement (CEGAR) automatic timing synthesis Umeno, Shinya Event Order Abstraction for Parametric Real-Time System Verification |
| title | Event Order Abstraction for Parametric Real-Time System Verification |
| title_full | Event Order Abstraction for Parametric Real-Time System Verification |
| title_fullStr | Event Order Abstraction for Parametric Real-Time System Verification |
| title_full_unstemmed | Event Order Abstraction for Parametric Real-Time System Verification |
| title_short | Event Order Abstraction for Parametric Real-Time System Verification |
| title_sort | event order abstraction for parametric real time system verification |
| topic | parametric verification event-based approach counter-example guided abstraction refinement (CEGAR) automatic timing synthesis |
| url | http://hdl.handle.net/1721.1/41891 |
| work_keys_str_mv | AT umenoshinya eventorderabstractionforparametricrealtimesystemverification |