Abstract
A powerful methodology for scenario-based specification of reactive systems is described, in which the behavior is “played in” directly from the system’s GUI or some abstract version thereof, and can then be “played out”. The approach is supported and illustrated by a tool, which we call the play-engine. As the behavior is played in, the play-engine automatically generates a formal version in an extended version of the language of live sequence charts (LSCs). As they are played out, it causes the application to react according to the universal (“must”) parts of the specification; the existential (“may”) parts can be monitored to check their successful completion. Play-in is a user-friendly high-level way of specifying behavior and play-out is a rather surprising way of working with a fully operational system directly from its inter-object requirements. The ideas appear to be relevant to many stages of system development, including requirements engineering, specification, testing, analysis and implementation.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Altia Design & Altia FacePlate, web page: http://www.altia.com
Alur, R., Henzinger, T.: Real-time System = Discrete System + Clock Variables. Software Tools for Technology Transfer 1: 86–109 , 1997
Amyot, D., Eberlein, A.: An Evaluation of Scenario Notations for Telecommunication Systems Development. In: Int. Conf. on Telecommunication Systems, 2001
Bharadwaj, R., Heitmeyer, C.: Model Checking Complete Requirements Specifications Using Abstraction. Automated Software Engineering, 6(1): 37–68, January 1999
Broy, M., Krüger, I.: Interaction Interfaces – Towards a Scientific Foundation of a Methodological Usage of Message Sequence Charts. In: Staples, J., Hinchey, M.G., Liu, S. (eds.) Formal Engineering Methods, IEEE Computer Society, 1998, pp. 2–15
Boger, M., Baier, T., Wienberg, F., Lamersdorf, W.: Extreme Modeling. In: Extreme Programming and Flexible Processes in Software Engineering – XP2000. Addison Wesley, 6 2000
Microsoft COM, web page: http://www.microsoft.com/com
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19(1) 2001. Preliminary version in: Ciancarini, P., Fantechi, A., Gorrieri, R. (eds.) Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS’99), Kluwer Academic Publishers, 1999, pp. 293–312
Dromey, R.: Genetic Software Engineering. Manuscript, 2001
e-SIM Rapid, web page http://www.e-sim.com/home/
Macromedia Flash, web page: http://www.macromedia.com/software/flash/
Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Prog., 8: 231–274, 1987. (Preliminary version: Tech. Report CS84-05, The Weizmann Institute of Science, Rehovot, Israel, February 1984.)
Harel, D.: From Play-In Scenarios to Code: An Achievable Dream. IEEE Computer, 34(1): 53–60, January 2001
Harel, D., Gery, E.: Executable Object Modeling with Statecharts. IEEE Computer, 30(7): 31–42, 1997
Harel, D., Koren, Y.: Drawing Graphs with Non-Uniform Vertices. In: Proc. of Working Conference on Advanced Visual Interfaces (AVI’02). ACM Press, 2002, pp. 157–166
Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Foundations of Computer Science (IJFCS)., 13(1): 5–51, Febuary 2002. (Also, Proc. Fifth Int. Conf. on Implementation and Application of Automata (CIAA 2000), July 2000, Lecture Notes in Computer Science, Springer-Verlag, 2000.)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart Play-Out of Behavioral Requirements. In: Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD’02), Portland, Oregon, 2002, pp. 378–398. Also available as Tech. Report MCS02-08, Weizmann Institute of Science, 2002
Harel, D., Marelly, R.: Come, Let’s Play: An Executable Scenario-Based Approach to Reactive Systems. (tentative title), manuscript, 2002
Harel, D., Marelly, R.: Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In: Proc. 10th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS’02), Fort Worth, Texas, 2002, pp. 193–202
Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, 1998. Early version titled: The Languages of STATEMATE. Technical Report, i-Logix, Inc., Andover, MA (250 pp.), 1991
Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R.: SCR*: A Toolset for Specifying and Analyzing Software Requirements. In: Hu, A., Vardi, e.M.Y. (eds.) Intl. Conference on Computer Aided Verification (CAV’98), Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, New York, 1998, pp. 5–51
Heymans, P., Dubois, E.: Scenario-Based Techniques for Supporting the Elaboration and the Validation of Formal Requirements. Requirements Engineering Journal 3: 202–218, Springer-Verlag, 1998
I-Logix,Inc., products web page: http://www.ilogix.com/fs_prod.htm
Jacobson, I.: Object-Oriented Software Engineering: A Use Case Driven Approach. Addison-Wesley, Reading, MA, 1992
Krüger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to Statecharts. Proc. DIPES’98, Kluwer, 1999
Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal Logic for Live Sequence Charts. Technical report, Weizmann Institute, 2000
Lettrari, M., Klose, J.: Scenario-Based Monitoring and Testing of Real-Time UML Models. In: 4th Int. Conf. on the Unified Modeling Language, Toronto, Lecture Notes in Computer Science, vol. 2185, October 2001, pp. 317–328
Magee, J., Kramer, J.: Concurrency – State Models & Java Programs. John Wiley & Sons, Chichester, 1999
Magee, J., Pryce, N., Giannakopoulou, D., Kramer, J.: Graphical Animation of Behavior Models. 22nd Int. Conf. on Soft. Eng. (ICSE’00), Limeric, Ireland, 2000
Marelly, R.: Specifying and Executing Behavioral Requirements: The Play-In/Play-Out Approach. PhD thesis, The Weizmann Institute of Science, 2002
Marelly, R., Harel, D., Kugler, H.: Multiple Instances and Symbolic Variables in Executable Sequence Charts. In: Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’02), Seattle, WA, 2002, pp. 83–100. Also available as Tech. Report MCS02-05 , Weizmann Institute of Science, 2002
Özcan, M., Parry, P., Morrey, I., Siddiqi, J.: Visualization of Executable Formal Specifications for User Validation. Ann. Soft. Eng., 3: 131–155, 1997
Pnueli, A.: The Temporal Semantics of Concurrent Programs. Theoretical Computer Science, 13: 1–20, 1981
Pryce, N., Magee, J.: SceneBeans: A Component-Based Animation Framework for Java. http://www-dse.doc.ic.ac.uk/Software/SceneBeans/
Rational,Inc., web page: http://www.rational.com
Robinson, J.: Logic: Form and Function, chap. 11. North-Holland, 1979, pp. 182–198
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading, MA, 1999
Schlor, R., Damm, W.: Specification and Verification of System-Level Hardware Designs using Timing Diagram. In: Proc. European Conference on Design Automation. IEEE Computer Society Press, Paris, France, 1993, pp. 518–524
Selic, B., Gullekson, G., Ward, P.: Real-Time Object-Oriented Modeling. John Wiley & Sons, New York, 1994
Siddiqi, J.I., Morrey, I.C., Roast, C.R., Ozcan, M.B.: Towards Quality Requirements via Animated Formal Specifications. Ann. Soft. Eng., 3: 131–155, 1997
Suzuki, J., Yamamoto, Y.: Extending UML for Modelling Reflective Software Components. In: France, R., Rumpe, B. (eds.) UML’99 – The Unified Modeling Language. Beyond the Standard. Second International Conference, Fort Collins, CO, USA, October 28–30 1999, Proceedings, Lecture Notes in Computer Science, vol. 1723. Springer, New York, 1999, pp. 220–235
Uchitel, S., Kramer, J., Magee, J.: Detecting Implied Scenarios in Message Sequence Chart Specifications. In: 9th European Software Engineering Conferece and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (ESEC/FSE’01). Vienna, Austria, September 2001
Documentation of the Unified Modeling Language (UML), available from the Object Management Group(OMG): http://www.omg.org
Web page: http://www.xml.com
Web page: http://www.extremeprogramming.org
Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva, 1996
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Harel, D., Marelly, R. Specifying and executing behavioral requirements: the play-in/play-out approach. Softw Syst Model 2, 82–107 (2003). https://doi.org/10.1007/s10270-002-0015-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10270-002-0015-5