A verification system for timed interval calculus

ABSTRACT

Timed Interval Calculus (TIC) is a highly expressive set-based notation for specifying and reasoning about embedded real-time systems. However, it lacks mechanical proving support, as its verification usually involves infinite time intervals and continuous dynamics. In this paper, we develop a system based on a generic theorem prover, Prototype Verification System (PVS), to assist formal verification of TIC at a high grade of automation. TIC semantics has been constructed by the PVS typed higher-order logic. Based on the encoding, we have checked all TIC reasoning rules and discovered subtle flaws. A translator has been implemented in Java to automatically transform TIC models into PVS specifications. A collection of supplementary rules and PVS strategies has been defined to facilitate the rigorous reasoning of TIC models with functional and non-functional (for example, real-time) requirements at the interval level. Our approach is generic and can be applied further to support other real-time notations.

REFERENCES

• 1: R. W. Butler. Formalization of the Integral Calculus in the PVS Theorem Prover. Technical report, NASA Langley Research Center, Hampton, Virginia, October 2004.
• 2: A. Cerone. Axiomatisation of an Interval Calculus for Theorem Proving. Electronic Notes Theoretical Computer Science, 42, 2001.
• 3: G. Chakravorty and P. K. Pandya. Digitizing Interval Duration Logic. In Computer Aided Verification, pages 167--179, 2003.
• 4: C. Chen, J. S. Dong, and J. Sun. Verification System for TIC. http://www.comp.nus.edu.sg/~chenchun/TIC2PVS, 2007.
• 5: Betty H. C. Cheng , Joanne M. Atlee, Research Directions in Requirements Engineering, 2007 Future of Software Engineering, p.285-303, May 23-25, 2007 [doi>10.1109/FOSE.2007.17]
• 6: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 7: Jeremy E. Dawson , Rajeev Goré, Machine-Checking the Timed Interval Calculus, Proceedings of the 15th Australian Joint Conference on Artificial Intelligence: Advances in Artificial Intelligence, p.95-106, December 02-06, 2002
• 8: B. Dutertre and M. Sorea. Timed Systems in SAL. Technical report, SRI International, 2004.
• 9: C. J. Fidge , I. J. Hayes , B. P. Mahony, Defining Differentiation and Integration in Z, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.64, December 09-11, 1998
• 10: Colin J. Fidge , Ian J. Hayes , A. P. Martin , Axel Wabenhorst, A Set-Theoretic Model for Real-Time Specification and Reasoning, Proceedings of the Mathematics of Program Construction, p.188-206, June 15-17, 1998
• 11: S. T. Heilmann. Proof Support for Duration Calculus. PhD thesis, Department of Information Technology, Technical University of Denmark, 1999.
• 12: T. A. Henzinger and J. Sifakis. The Embedded Systems Design Challenge. In Formal Methods, pages 1--15, 2006.
• 13: Brendan P. Mahony , Ian J. Hayes, A Case-Study in Timed Refinement: A Mine Pump, IEEE Transactions on Software Engineering, v.18 n.9, p.817-826, September 1992 [doi>10.1109/32.159841]
• 14: Aloysius K. Mok , Chan-Gun Lee , Honguk Woo , Prabhudev Konana, The Monitoring of Timing Constraints on Time Intervals, Proceedings of the 23rd IEEE Real-Time Systems Symposium (RTSS'02), p.191, December 03-05, 2002
• 15: C. Muñoz, V. Carreño, and G. Dowek. Formal Analysis of the Operational Concept for the Small Aircraft Transportation System. In Rigorous Development of Complex Fault-Tolerant Systems, pages 306--325, 2006.
• 16: Xavier Nicollin , Joseph Sifakis , Sergio Yovine, From ATP to Timed Graphs and Hybrid Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.549-572, June 03-07, 1991
• 17: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 18: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 19: John M. Rushby, Theorem Proving for Verification, Proceedings of the 4th Summer School on Modeling and Verification of Parallel Processes, p.39-57, June 19-23, 2000
• 20: Jens Ulrik Skakkebæk , Natarajan Shankar, Towards a Duration Calculus Proof Assistant in PVS, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.660-679, September 19-23, 1994
• 21: A. Tiwari, N. Shankar, and J. M. Rushby. Invisible Formal Methods for Embedded Control Systems. Proceedings of the IEEE, 91(1):29--39, 2003.
• 22: Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 23: Yue Yu , Shangping Ren , Ophir Frieder, Prediction of Timing Constraint Violation for Real-Time Embedded Systems with Known Transient Hardware Failure Distribution Model, Proceedings of the 27th IEEE International Real-Time Systems Symposium, p.454-466, December 05-08, 2006 [doi>10.1109/RTSS.2006.33]
• 24: Chaochen Zhou , Michael R. Hansen, Duration Calculus: A Formal Approach to Real-Time Systems (Monographs in Theoretical Computer Science. an Eatcs Seris), SpringerVerlag, 2004
• 25: Zhou Chaochen , Li Xiaoshan, A mean value calculus of durations, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 26: Zhou Chaochen , Anders P. Ravn , Michael R. Hansen, An Extended Duration Calculus for Hybrid Real-Time Systems, Hybrid Systems, p.36-59, January 1993

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
      D.2.4 Software/Program Verification
          Subjects: Validation

General Terms:
Verification

Keywords:
pvs, real-time systems, specification language, theorem proving