Abstract
Smart play-out is a method for executing declarative scenario-based specifications, which utilizes powerful computation methods to compute safe supersteps, thus helping to avoid violations that may be caused by naïve execution. Major challenges for smart play-out are performance and scalability. In this work we show how to accelerate smart play-out by adapting and applying ideas inspired by formal verification and compiler optimization. Specifically, we present an algorithm that can reduce the size of the specification considered for smart play-out, while maintaining soundness and completeness. Experimental results show significant performance improvements and thus open the way to the application of smart play-out to large scenario-based programs.
This research was partially supported by the John von Neumann Minerva Center for the Development of Reactive Systems at the Weizmann Institute of Science, and by an Advanced Research Grant from the European Research Council (ERC) under the European Community’s 7th Framework Programme (FP7/2007-2013).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. IEEE Trans. Software Eng. 29(7), 623–633 (2003)
Broy, M.: A Semantic and Methodological Essence of Message Sequence Charts. Sci. Comput. Program. 54(2-3), 213–256 (2005)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. J. on Form. Meth. in Sys. Design 19(1), 45–80 (2001)
Harel, D., Marelly, R.: Come Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Uchitel, S., Kramer, J., Magee, J.: Synthesis of Behavioral Models from Scenarios. IEEE Trans. Software Eng. 29(2), 99–115 (2003)
ITU: International Telecommunication Union Recommendation Z.120: Message Sequence Charts. Technical report (1996)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart Play-out of Behavioral Requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002)
Harel, D., Kugler, H., Maoz, S., Segall, I.: How Hard is Smart Play-Out? On the Complexity of Verification-Driven Execution. In: Perspectives in Concurrency Theory (Festschrift for P.S. Thiagarajan), pp. 208–230. University Press, India (2009)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Harel, D., Kugler, H., Maoz, S., Segall, I.: Accelerating Smart Play-Out. Technical Report, Weizmann Institute of Science (2009)
Harel, D., Segall, I.: Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 485–499. Springer, Heidelberg (2007)
Combes, P., Harel, D., Kugler, H.: Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool. Int. J. Soft. Sys. Mod (SoSyM) 7(2), 157–175 (2008)
Callahan, D., Cooper, K.D., Kennedy, K., Torczon, L.: Interprocedural Constant Propagation. In: Proc. SIGPLAN Symp. on Compiler Construction (CC 1986), pp. 152–161. ACM, New York (1986)
Korel, B., Yalamanchili, S.: Forward Computation of Dynamic Program Slices. In: Proc. ACM SIGSOFT Int. Symp. on Software Testing and Analysis (ISSTA 1994), pp. 66–79. ACM, New York (1994)
Krüger, I.: Capturing Overlapping, Triggered, and Preemptive Collaborations Using MSCs. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 387–402. Springer, Heidelberg (2003)
Pezzé, M., Young, M.: Software Testing and Analysis: Process, Principles and Techniques. John Wiley & Sons, Chichester (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harel, D., Kugler, H., Maoz, S., Segall, I. (2010). Accelerating Smart Play-Out. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds) SOFSEM 2010: Theory and Practice of Computer Science. SOFSEM 2010. Lecture Notes in Computer Science, vol 5901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11266-9_40
Download citation
DOI: https://doi.org/10.1007/978-3-642-11266-9_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11265-2
Online ISBN: 978-3-642-11266-9
eBook Packages: Computer ScienceComputer Science (R0)