Action Language: a specification language for model checking reactive systems

ABSTRACT

We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statecharts, RSML and SCR—similar to an assembly language between a microprocessor and a programming language. We show that Action Language translations of Statecharts and SCR specifications are compact and they preserve the structure of the original specification. Action Language allows specification of both synchronous and asynchronous systems. It also supports modular specifications to enable compositional model checking.

REFERENCES

• 1: 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]
• 2: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305]
• 3: R. Bharadwaj and C. Heitmeyer. Verifying SCR requirements speci cations using state exploration. In Proceedings of First ACM SIGPLAN Workshop on Automatic Analysis of Software, January 1997.
• 4: Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999 [doi>10.1023/A:1008697817793]
• 5: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 6: Tevfik Bultan , Jeffrey Fischer , Richard Gerber, Compositional verification by model checking for counter-examples, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.224-238, January 08-10, 1996, San Diego, California, United States
• 7: Tevfik Bultan , Richard Gerber , Christopher League, Verifying systems with integer constraints and Boolean predicates: a composite approach, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.113-123, March 02-04, 1998, Clearwater Beach, Florida, United States
• 8: J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 10 20 states and beyond. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pages 428{439, January 1990.
• 9: 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]
• 10: 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]
• 11: 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]
• 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: Alberto Coen-Porisini , Carlo Ghezzi , Richard A. Kemmerer, Specification of realtime systems using ASTRAL, IEEE Transactions on Software Engineering, v.23 n.9, p.572-598, September 1997 [doi>10.1109/32.629494]
• 14: Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997 [doi>10.1145/244795.244800]
• 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: Constance L. Heitmeyer , Ralph D. Jeffords , Bruce G. Labaw, Automated consistency checking of requirements specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.3, p.231-261, July 1996 [doi>10.1145/234426.234431]
• 17: Constance Heitmeyer , James Kirby, Jr. , Bruce Labaw , Myla Archer , Ramesh Bharadwaj, Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications, IEEE Transactions on Software Engineering, v.24 n.11, p.927-948, November 1998 [doi>10.1109/32.730543]
• 18: 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]
• 19: 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]
• 20: 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]
• 21: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 22: A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45{60, 1981.
• 23: T. Sreemani and J. M. Atlee. Feasibility of model checking software requirements: A case study. In Proceedings of the 11th Annual Conference Computer Assurance, pages 77{88, June 1996.
• 24: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of First IEEE Symposium on Logic Computer Science, pages 322{331, 1986.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

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

General Terms:
Design, Languages, Measurement, Performance, Reliability, Theory, Verification

Keywords:
model checking, reactive systems, specification languages