Reasoning about real-time statecharts in the presence of semantic variations

ABSTRACT

This paper describes a framework that allows for reasoning about and verification of concurrent statecharts with real-time constraints subject to semantic variations. The major problems addressed by this paper include the capture of multiple semantic variations of real-time statecharts, and the use of the resulting semantics for further analysis. Our solution is based on a theoretical framework involving a two-dimensional temporal logic that is used to independently capture flow of control through statecharts as well as flow of time. The independence of these dimensions, along with the high-level nature of temporal logic allows for simple adaptation to alternate semantics of statecharts as well as real-time models. The paper defines our logic, shows how the semantics of real-time statecharts can be expressed in this formalism, and describes our tools for capturing and reasoning about these semantics. The underlying goal is the formal analysis of real-time software behavior in a way that captures designer intentions.

REFERENCES

• 1: Rajeev Alur, Timed Automata, Proceedings of the 11th International Conference on Computer Aided Verification, p.8-22, July 06-10, 1999
• 2: T. Arons, J. Hooman, H. Kugler, A. Pnueli, and M. van der Zwaag. Deductive verification of UML models in TLPVS. In UML, pages 335--349, 2004.
• 3: Sérgio Vale Aguiar Campos , Edmund M. Clarke , Marius Minea, The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems, Proceedings of the 9th International Conference on Computer Aided Verification, p.452-455, June 22-25, 1997
• 4: William Chan , Richard J. Anderson , Paul Beame , David H. Jones , David Notkin , William E. Warner, Decoupling synchronization from local control for efficient symbolic model checking of statecharts, Proceedings of the 21st international conference on Software engineering, p.142-151, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302460]
• 5: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 6: Alexandre David , M. Oliver Möller , Wang Yi, Formal Verification of UML Statecharts with Real-Time Extensions, Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering, p.218-232, April 08-12, 2002
• 7: K. Diethers, U. Goltz, and M. Huhn. Model checking UML statecharts with time. In Workshop on Critical Systems Development with UML, 2002.
• 8: Laura K. Dillon , R. E. Kurt Stirewalt, Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components, IEEE Transactions on Software Engineering, v.29 n.2, p.133-150, February 2003 [doi>10.1109/TSE.2003.1178052 ]
• 9: K. Fuhrmann and J. Hiemer. Formal verification of STATEMATE-statecharts. Technical report, ESPRESS Project Technical Report, 2001.
• 10: C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
• 11: David Harel, Recurring Dominoes: Making the Highly Undecidable Highly Understandable (Preliminary Report), Proceedings of the 1983 International FCT-Conference on Fundamentals of Computation Theory, p.177-194, August 21-27, 1983
• 12: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9 ]
• 13: David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
• 14: Alexander Knapp , Stephan Merz , Christopher Rauh, Model Checking - Timed UML State Machines and Collaborations, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.395-416, September 09-12, 2002
• 15: Fred Kröger, Temporal logic of programs, Springer-Verlag New York, Inc., New York, NY, 1987
• 16: G. Kwon. Rewrite rules and operational semantics for model checking UML statecharts. In 3rd International Conference on the Unified Modeling Language (UML), pages 528--540, 2000.
• 17: 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, October 1997.
• 18: D. Latella, I. Majzik, and M. Massink. Automatic verification of a behavioral subset of UML statechart diagrams using the SPIN model checker. Formal Aspects of Computing, 11(6):637--664, 1999.
• 19: Luigi Lavazza , Gabriele Quaroni , Matteo Venturelli, Combining UML and formal notations for modelling real-time systems, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 20: J. Lilius and I. P. Paltor. Formalising UML state machines for model checking. In Second International Conference on the Unified Modeling Language (UML), pages 430--445, 1999.
• 21: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 22: Jianwei Niu , Joanne M. Atlee , Nancy A. Day, Composable semantics for model-based notations, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587074]
• 23: Object Management Group. UML 1.4 with Action Semantics, Final Adopted Specification, 1999.
• 24: Object Management Group. UML Profile for Schedulability, Performance, and Time Specification, Draft Adopted Specification, January 2002.
• 25: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 26: Á. Schmidt and D. Varró. CheckVML: A tool for model checking visual modeling languages. In 6th International Conference on the Unified Modeling Language (UML), pages 92--95, 2003.
• 27: Subash Shankar, A Semantic Model of Real-Time UML, Proceedings of the 4th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering, p.573-577, October 21-25, 2002
• 28: S. Shankar and S. Asa. Formal semantics of UML with real-time constructs. In UML, pages 60--75, 2003.
• 29: I. Traore, D. B. Aredo, and H. Ye. An integrated framework for formal development of open distributed systems. Information and Software Technology, 46(5):281--286, April 2004.
• 30: Michael von der Beeck, A Comparison of Statecharts Variants, 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.128-148, September 19-23, 1994

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: State diagrams
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Verification

Keywords:
model checking, semantics, statecharts, temporal logics, theorem proving