Synthesizing reactive systems from LSC requirements using the play-engine

ABSTRACT

Live Sequence Charts (LSCs) is a scenario-based language for modeling object-based reactive systems with liveness properties. A tool called the Play-Engine allows users to create LSC requirements using a point-and-click interface and generate executable traces using features called play-out and smart play-out. Finite executable trace fragments called super-steps are generated by smart play-out in response to user inputs. Each super-step is guaranteed not to violate the LSC requirements, provided one exists. However, non-violation is not guaranteed beyond each individual super-step. In this work, we demonstrate a powerful extension to smart play-out which produces only traces that are guaranteed not to violate the LSC requirements, provided the requirements are realizable. Using this method, we may synthesize correct executable programs directly from LSC requirements.

REFERENCES

• 1: E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In IFAC Symposium on System Structure and Control, pages 469--474. Elsevier, 1998.
• 2: Werner Damm , David Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design, v.19 n.1, p.45-80, July 2001 [doi>10.1023/A:1011227529550]
• 3: David Harel , Hillel Kugler, Synthesizing State-Based Object Systems from LSC Specifications, Revised Papers from the 5th International Conference on Implementation and Application of Automata, p.1-33, July 24-25, 2000
• 4: David Harel , Hillel Kugler , Rami Marelly , Amir Pnueli, Smart Play-out of Behavioral Requirements, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.378-398, November 06-08, 2002
• 5: David Harel , Rami Marelly, Come, Let's Play: Scenario-Based Programming Using LSC's and the Play-Engine, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 6: N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'06), volume 3855 of Lect. Notes in Comp. Sci., pages 364--380. Springer-Verlag, 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools
      D.2.2 Design Tools and Techniques
          Subjects: Object-oriented design methods
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Design, Languages, Verification

Keywords:
controller synthesis, live sequence charts, reactive systems