tailieunhanh - Event Order Abstraction for Parametric Real-Time System Verification

Some beautiful and famous countryside sites are at risk of being over-used for large-scale walks. This kind of activity brings hundreds of tramping feet and a hubbub of noise and bustle which can destroy the very beauty and atmosphere for which the place is famous. Other sites and routes are much more robust and lend themselves happily to throngs of people all enjoying themselves at the same place at the same time. Choose your event site wisely. | lUii Computer Science and Artificial Intelligence Laboratory Technical Report October 19 2008 MIT-CSAIL-TR-2008-048 massa chusetts institute of technology Cambridge ma 02139 usa CSAI L Event Order Abstraction for Parametric Real-Time System Verification Shinya Umeno Event Order Abstraction for Parametric Real-Time System Verification Shinya Umeno Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology 32 Vassar St Cambridge MA 02139 USA Abstract 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 call 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 .