Abstract
The behavior of open reactive systems is best described in an assume-guarantee style specification: a system guarantees certain prescribed behavior provided that its environment follows certain given assumptions. Scenario-based modeling languages, such as variants of message sequence charts, have been used to specify reactive systems behavior in a visual, modular, intuitive way. However, none have yet provided full support for assume-guarantee style specifications.
In this paper we present assume-guarantee scenarios, which extend live sequence charts (lsc) – a visual, expressive, scenario-based language – syntax and semantics, with an explicit distinction between system and environment entities and with support not only for safety and liveness system guarantees but also for safety and liveness environment assumptions. Moreover, the semantics is defined using a reduction to gr(1), a fragment of ltl that enables game-based, symbolic, efficient synthesis of a correct-by-construction controller.
This research was supported by The John von Neumann Minerva Center for the Development of Reactive Systems at the Weizmann Institute of Science. In addition, part of this research was funded by an Advanced Research Grant awarded to David Harel of the Weizmann Institute from the European Research Council (ERC) under the European Community’s 7th Framework Programme (FP7/2007-2013).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alfonso, A., Braberman, V.A., Kicillof, N., Olivero, A.: Visual timed event scenarios. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) ICSE, pp. 168–177. IEEE Computer Society (2004)
Autili, M., Inverardi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Autom. Softw. Eng. 14(3), 293–340 (2007)
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for Playing Games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. Journal of Computer and System Sciences 78(3), 911–938 (2012)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19(1), 45–80 (2001)
Greenyer, J.: Scenario-based Design of Mechatronic Systems. PhD thesis, University of Paderborn, Department of Computer Science (2011)
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., Maoz, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and Systems Modeling 7(2), 237–252 (2008)
Harel, D., Maoz, S., Szekely, S., Barkan, D.: PlayGo: towards a comprehensive tool for scenario based programming. In: ASE, pp. 359–360. ACM (2010)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSC’s and the Play-Engine. Springer (2003)
Harel, D., Pnueli, A.: On the Development of Reactive Systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. ATO ASI Series, vol. F-13, pp. 477–498. Springer (1985)
Harel, D., Segall, I.: Synthesis from scenario-based specifications. Journal of Computer and System Sciences 78(3), 970–980 (2012)
Haugen, Ø., Husa, K.E., Runde, R.K., Stølen, K.: STAIRS towards formal design with sequence diagrams. Software and Systems Modeling 4(4), 355–367 (2005)
Jackson, M.: The world and the machine. In: Perry, D.E., Jeffrey, R., Notkin, D. (eds.) ICSE, pp. 283–292. ACM (1995)
Knapp, A., Wuttke, J.: Model Checking of UML 2.0 Interactions. In: Kühne, T. (ed.) MoDELS 2006. LNCS, vol. 4364, pp. 42–51. Springer, Heidelberg (2007)
Könighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: FMCAD, pp. 152–159. IEEE (2009)
Krüger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to Statecharts. In: DIPES, pp. 61–72 (1998)
Kugler, H., Plock, C., Pnueli, A.: Controller Synthesis from LSC Requirements. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 79–93. Springer, Heidelberg (2009)
Kugler, H., Segall, I.: Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 77–91. Springer, Heidelberg (2009)
Kupferman, O., Vardi, M.Y.: Module Checking Revisited. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 36–47. Springer, Heidelberg (1997)
Manna, Z., Pnueli, A.: The temporal logic of concurrent and reactive systems: specification. Springer (1992)
Maoz, S., Harel, D.: From multi-modal scenarios to code: compiling LSCs into AspectJ. In: SIGSOFT FSE, pp. 219–230. ACM (2006)
Maoz, S., Harel, D., Kleinbort, A.: A compiler for multimodal scenarios: Transforming LSCs into AspectJ. ACM Trans. Softw. Eng. Methodol. 20(4), 18 (2011)
Maoz, S., Sa’ar, Y.: Counter play-out: Debugging unrealizable scenario-based specifications (in preparation, 2012)
Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS, pp. 275–284. IEEE Computer Society (2006)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)
Pnueli, A., Sa’ar, Y., Zuck, L.D.: Jtlv: A Framework for Developing Verification Algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 171–174. Springer, Heidelberg (2010)
Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control 54(1/2), 121–141 (1982)
Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: ICSE, pp. 314–323. ACM (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maoz, S., Sa’ar, Y. (2012). Assume-Guarantee Scenarios: Semantics and Synthesis. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds) Model Driven Engineering Languages and Systems. MODELS 2012. Lecture Notes in Computer Science, vol 7590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33666-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-33666-9_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33665-2
Online ISBN: 978-3-642-33666-9
eBook Packages: Computer ScienceComputer Science (R0)