Take a look at the new version of this page: [ beta version ]. Tell us what you think.

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 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 [13]. We also summarize three other case studies, a biphase mark protocol, the IEEE 1394 root contention protocol, and the Fischer mutual exclusion algorithm.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: Rajeev Alur , Thomas A. Henzinger , Moshe Y. Vardi, Parametric real-time reasoning, Proceedings of the twenty-fifth annual ACM symposium on Theory of computing, p.592-601, May 16-18, 1993, San Diego, California, United States [doi>10.1145/167088.167242]
• 3: Aurore Annichini , Ahmed Bouajjani , Mihaela Sighireanu, TReX: A Tool for Reachability Analysis of Complex Systems, Proceedings of the 13th International Conference on Computer Aided Verification, p.368-372, July 18-22, 2001
• 4: Eugene Asarin , Oded Maler , Amir Pnueli, On Discretization of Delays in Timed Automata and Digital Circuits, Proceedings of the 9th International Conference on Concurrency Theory, p.470-484, September 08-11, 1998
• 5: D. Bosnacki. Digitization of timed automata. In Proc. of FMICS 99, 1999.
• 6: H. Bowman, G. Faconti, J.-P. Katoen, D. Latella, and M. Massink. Automatic verification of a lip-synchronisation protocol using uppaal. Formal Aspects of Computing, 10(5-6):550--575, 1998.
• 7: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 8: S. R. Dalal , A. Jain , N. Karunanithi , J. M. Leaton , C. M. Lott , G. C. Patton , B. M. Horowitz, Model-based testing in practice, Proceedings of the 21st international conference on Software engineering, p.285-294, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302640]
• 9: L. M. de Moura, S. Owre, H. Rueß, J. M. Rushby, N. Shankar, M. Sorea, and A. Tiwari. SAL 2. In Proc. of CAV 2004, volume 3114 of Lecture Notes in Computer Science, pages 496--500. Springer, 2004.
• 10: Jeremy Dick , Alain Faivre, Automating the Generation and Sequencing of Test Cases from Model-Based Specifications, Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods, p.268-284, April 19-23, 1993
• 11: Goran Frehse , Sumit Kumar Jha , Bruce H. Krogh, A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata, Proceedings of the 11th international workshop on Hybrid Systems: Computation and Control, April 22-24, 2008, St. Louis, MO, USA [doi>10.1007/978-3-540-78929-1_14]
• 12: K. Havelund , A. Skou , K. G. Larsen , K. Lund, Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL, Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), p.2, December 03-05, 1997
• 13: C. Heitmeyer , N. Lynch, The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems, Massachusetts Institute of Technology, Cambridge, MA, 1994
• 14: T. Henzinger, J. Preussig, and H. Wong-Toi. Some lessons from the HYTECH experience. In Proc. of the 40th Annual Conference on Decision and Control, pages 2887--2892. IEEE Computer Society Press, 2001.
• 15: T. A. Henzinger, The theory of hybrid automata, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.278, July 27-30, 1996
• 16: Thomas A. Henzinger , Zohar Manna , Amir Pnueli, Timed Transition Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.226-251, June 03-07, 1991
• 17: Thomas A. Henzinger , Zohar Manna , Amir Pnueli, What Good Are Digital Clocks?, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.545-558, July 13-17, 1992
• 18: Thomas Hune , Judi Romijn , Mariëlle Stoelinga , Frits W. Vaandrager, Linear Parametric Model Checking of Timed Automata, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.189-203, April 02-06, 2001
• 19: Dilsun K. Kaynar , Nancy Lynch , Roberto Segala , Frits Vaandrager, The Theory of Timed I/O Automata (Synthesis Lectures in Computer Science), Morgan & Claypool Publishers, 2006
• 20: K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134--152, 1997.
• 21: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 22: O. Maler , S. Yovine, Hardware timing verification using KRONOS, Proceedings of the 7th Israeli Conference on Computer-Based Systems and Software Engineering, p.23, June 10-12, 1996
• 23: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 24: Michael Merritt , Francesmary Modugno , Marc R. Tuttle, Time-Constrained Automata (Extended Abstract), Proceedings of the 2nd International Conference on Concurrency Theory, p.408-423, August 26-29, 1991
• 25: J. S. Moore. A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Formal Aspects of Computing, 6(1):60--91, 1994.
• 26: Joël Ouaknine , James Worrell, Revisiting Digitization, Robustness, and Decidability for Timed Automata, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.198, June 22-25, 2003
• 27: D. P. L. Simons and M. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. International Journal on Software Tools for Technology Transfer, 3(4):469--485, 2001.
• 28: R. F. Lutje Spelberg , W. J. Toetenel, Parametric real-time model checking using splitting trees, Nordic Journal of Computing, v.8 n.1, p.88-120, Spring 2001
• 29: S. Umeno. Parametrically verifying embedded real-time protocols using event order abstraction. Technical report, Massachusetts Institute of Technology. To appear. (A conference version has been submitted for publication).
• 30: S. Umeno. Event order abstraction for parametric real-time system verification. Technical Report MIT-CSAIL-TR-2008-048, Massachusetts Institute of Technology, July 2008.
• 31: F. W. Vaandrager , A. L. de Groot, Analysis of a biphase mark protocol with Uppaal and PVS, Formal Aspects of Computing, v.18 n.4, p.433-458, November 2006 [doi>10.1007/s00165-006-0008-1]
• 32: Farn Wang, Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures, IEEE Transactions on Software Engineering, v.31 n.1, p.38-51, January 2005 [doi>10.1109/TSE.2005.13]
• 33: S. Yovine. KRONOS: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT), 1(1-2):123--133, 1997.
• 34: Dezhuang Zhang , Rance Cleaveland, Fast On-the-Fly Parametric Real-Time Model Checking, Proceedings of the 26th IEEE International Real-Time Systems Symposium, p.157-166, December 05-08, 2005 [doi>10.1109/RTSS.2005.22]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Mechanical verification

General Terms:
Algorithms, Design, Verification

Keywords:
automatic timing synthesis, counter-example guided abstraction refinement (cegar), event-based approach, parametric verification