Modular refinement of hierarchic reactive machines

ABSTRACT

Scalable formal analysis of reactive programs demands integration of modular reasoning techniques with existing analysis tools. Modular reasoning principles such as abstraction, compositional refinement, and assume-guarantee reasoning are well understood for architectural hierarchy that describes the communication structure between component processes, and have been shown to be useful. In this paper, we develop the theory of modular reasoning for behavior hierarchy that describes control structure using hierarchic modes. From Statecharts to UML, behavior hierarchy has been an integral component of many software design languages, but only syntactically. We present the hierarchic reactive modules language that retains powerful features such as nested modes, mode reuse, exceptions, group transitions, history, and conjunctive modes, and yet has a semantic notion of mode hierarchy. We present an observational trace semantics for modes that provides the basis for mode refinement. We show the refinement to be compositional with respect to the mode constructors, and develop an assume-guarantee reasoning principle.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.507-535, May 1995 [doi>10.1145/203095.201069]
• 2: R. Alur , L. de Alfaro , R. Grosu , T. A. Henzinger , M. Kang , C. M. Kirsch , R. Majumdar , F. Mang , B. Y. Wang, JMOCHA: a model checking tool that exploits design structure, Proceedings of the 23rd International Conference on Software Engineering, p.835-836, May 12-19, 2001, Toronto, Ontario, Canada
• 3: Rajeev Alur , Radu Grosu , M. McDougall, Efficient Reachability Analysis of Hierarchical Reactive Machines, Proceedings of the 12th International Conference on Computer Aided Verification, p.280-295, July 15-19, 2000
• 4: Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999 [doi>10.1023/A:1008739929481]
• 5: Rajeev Alur , Bow-Yaw Wang, Verifying Network Protocol Implementations by Symbolic Refinement Checking, Proceedings of the 13th International Conference on Computer Aided Verification, p.169-181, July 18-22, 2001
• 6: Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.175-188, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 7: Gerd Behrmann , Kim Guldstrand Larsen , Henrik Reif Andersen , Henrik Hulgaard , Jørn Lind-Nielsen, Verification of Hierarchical State/Event Systems Using Reusability and Compositionality, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.163-177, March 22-28, 1999
• 8: Karthikeyan Bhargavan , Carl A. Gunter , Elsa L. Gunter , Michael Jackson , Davor Obradovic , Pamela Zave, The Village Telephone System: A Case Study in Formal Software Engineering, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, p.49-66, September 27-October 01, 1998
• 9: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 10: William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998 [doi>10.1109/32.708566]
• 11: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 12: Edmund M. Clarke , Robert P. Kurshan, Computer-aided verification, IEEE Spectrum, v.33 n.6, p.61-67, June 1996 [doi>10.1109/6.499951]
• 13: R. Grosu , G. Stefanescu , M. Broy , realistic applications., Visual Formalisms Revisited, Proceedings of the 1998 International Conference on Application of Concurrency to System Design, p.41, March 23-26, 1998
• 14: Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994 [doi>10.1145/177492.177725]
• 15: 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]
• 16: 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]
• 17: Harel, D., Pnueli, A., Schmidt, J., and Sherman, R. 1987. On the formal semantics of statecharts. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science. 54--64.
• 18: Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, You Assume, We Guarantee: Methodology and Case Studies, Proceedings of the 10th International Conference on Computer Aided Verification, p.440-451, June 28-July 02, 1998
• 19: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 20: Franz Huber , Bernhard Schätz , Alexander Schmidt , Katharina Spies, AutoFocus: A Tool for Distributed Systems Specification, Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.467-470, September 09-13, 1996
• 21: F. Jahanian , A. K.-L. Mok, A graph-theoretic approach for timing analysis and its implementation, IEEE Transactions on Computers, v.36 n.8, p.961-975, Aug. 1987 [doi>10.1109/TC.1987.5009519]
• 22: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 23: Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994 [doi>10.1109/32.317428]
• 24: Gerald Lüttgen , Michael von der Beeck , Rance Cleaveland, A compositional approach to statecharts semantics, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.120-129, November 06-10, 2000, San Diego, California, United States
• 25: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 26: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 27: Kenneth L. McMillan, A Compositional Rule for Hardware Design Refinement, Proceedings of the 9th International Conference on Computer Aided Verification, p.24-35, June 22-25, 1997
• 28: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 29: Amir Pnueli , M. Shalev, What is in a Step: On the Semantics of Statecharts, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.244-264, September 24-27, 1991
• 30: Bran Selic , Garth Gullekson , Paul T. Ward, Real-time object-oriented modeling, John Wiley & Sons, Inc., New York, NY, 1994
• 31: Eugene W. Stark, A Proof Technique for Rely/Guarantee Properties, Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, p.369-391, December 16-18, 1985
• 32: Andrew C. Uselton , Scott A. Smolka, A Compositional Semantics for Statecharts using Labeled Transition Systems, Proceedings of the Concurrency Theory, p.2-17, August 22-25, 1994

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: State diagrams

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages; Methodologies (e.g., object-oriented, structured)
      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
          Subjects: Specification techniques; Mechanical verification

General Terms:
Languages, Verification

Keywords:
Hierarchical state machines, assume-guarantee reasoning, compositional semantics, refinement