Navegar

Colección

Datos Estadísticas

Artículo

Sibay, G.E.; Braberman, V.; Uchitel, S.; Kramer, J. "Synthesizing modal transition systems from triggered scenarios" (2013) IEEE Transactions on Software Engineering. 39(7):975-1001
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional universal scenarios and some limited support for nonconditional existential scenarios. In this paper, we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behavior models, such as Labeled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems (MTS), an extension of labeled Transition Systems that can distinguish between required, unknown, and proscribed behavior to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behavior models through refinement, which complements an incremental elicitation process suitable for specifying behavior with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterize all the Labeled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis, and Modal Transition Systems supports behavior model elaboration. © 1976-2012 IEEE.

Registro:

Documento: Artículo
Título:Synthesizing modal transition systems from triggered scenarios
Autor:Sibay, G.E.; Braberman, V.; Uchitel, S.; Kramer, J.
Filiación:Department of Computing, Imperial College London, Huxley Building, 180 Queen's Gate, SW7 2B7 London, United Kingdom
Department of Computing, University of Buenos Aires, Ciudad Universitaria, Intendente Güiraldes 2160, Buenos Aires (C1428EGA), Argentina
Palabras clave:MTS; partial behavior models; Scenarios; synthesis; Labeled transition systems; Modal Transition Systems; MTS; Operational behavior; Partial behavior models; Scenario-based languages; Scenario-based specifications; Scenarios; Flowcharting; Semantics; Specification languages; Synthesis (chemical); Specifications
Año:2013
Volumen:39
Número:7
Página de inicio:975
Página de fin:1001
DOI: http://dx.doi.org/10.1109/TSE.2012.62
Título revista:IEEE Transactions on Software Engineering
Título revista abreviado:IEEE Trans Software Eng
ISSN:00985589
CODEN:IESED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v39_n7_p975_Sibay

Referencias:

  • Kruger, I., (2000) Distributed System Design with Message Sequence Charts, , PhD dissertation Technical Univ. of Munich
  • Uchitel, S., Kramer, J., Magee, J., Incremental elaboration of scenario-based specifications and behaviour models using implied scenarios (2004) ACM Trans. Software Eng. and Methodology, 13 (1), pp. 37-85
  • Harel, D., Marelly, R., (2003) Come Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine, , Springer
  • Bontemps, Y., Heymans, P., Schobbens, P.-Y., From live sequence charts to state machines and back: A guided tour (2005) IEEE Transactions on Software Engineering, 31 (12), pp. 999-1014. , DOI 10.1109/TSE.2005.137
  • Ziadi, T., Helouet, L., Jezequel, J.-M., Revisiting statechart synthesis with an algebraic approach (2004) Proc. 26th IEEE Int'l Conf. Software Eng, pp. 242-251
  • (2000) ITU Recommendation z.120: Message Sequence Charts
  • Sengupta, B., Cleaveland, R., Triggered message sequence charts (2006) IEEE Transactions on Software Engineering, 32 (8), pp. 587-607. , DOI 10.1109/TSE.2006.82
  • Damm, W., Harel, D., Lscs: Breathing life into message sequence charts (1999) Proc. Third Int'l Conf. Formal Methods for Open ObjectBased Distributed Systems, 139
  • Zachos, K., Maiden, N., Tosar, A., Rich-media scenarios for discovering requirements (2005) IEEE Software, 22 (5), pp. 89-97. , DOI 10.1109/MS.2005.134
  • Keller, R.M., Formal verification of parallel programs (1976) Comm. ACM, 19, pp. 371-384. , July
  • Milner, R., (1989) Communication and Concurrency, , Prentice-Hall
  • Larsen, K., Thomsen, B., A modal process logic (1988) Proc. Third Ann IEEE Symp. Logic in Computer Science, pp. 203-210
  • Larsen, K., Steffen, B., Weise, C., The methodology of modal constraints (1996) Formal Systems Specification, 1169, pp. 405-435
  • Huth, M., Jagadeesan, R., Schmidt, D., Modal transition systems: A foundation for three-valued program analysis (2001) Lecture Notes in Computer Science, (2028), pp. 155-169. , Programming Languages and Systems
  • Larsen, K.G., Steffen, B., Weise, C., A constraint oriented proof methodology based on modal transition systems (1995) Proc. First Int'l Workshop Tools and Algorithms for Construction and Analysis of Systems, pp. 13-28
  • Fischbein, D., Uchitel, S., On correct and complete merging of partial behaviour models (2008) Proc. SIGSOFT Conf. Foundations of Software Eng, pp. 297-307
  • Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) IEEE Trans. Software Eng, 3 (35), pp. 384-406. , May
  • Brunet, G., Chechik, M., Fischbein, D., D'Ippolito, N., Uchitel, S., Weak Alphabet Merging of Partial Behaviour Models, , ACM Trans. Software Eng. and Methodology
  • Bruns, G., Godefroid, P., Generalized model checking: Reasoning about partial state spaces (2000) Proc. 11th Int'l Conf. Concurrency Theory, pp. 168-182
  • Fischbein, D., D'Ippolito, N., Sibay, G., Uchitel, S., (2012) Modal Transition System Analyser (MTSA), , http://sourceforge.net/projects/mtsa/
  • Magee, J., Kramer, J., (1999) Concurrency-State Models, Java Programs, , John Wiley
  • Uchitel, S., Chechik, M., Merging partial behavioural models (2004) Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 43-52. , Twelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12
  • Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking, , MIT Press
  • Sibay, G., Uchitel, S., Braberman, V., Existential live sequence charts revisited (2008) Proc. 30th Int'l Conf. Software Eng, pp. 41-50
  • Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) Proc. Ninth European Software Eng. Conf, , Held Jointly with 11th ACM SIGSOFT Int'l Symp. Foundations of Software Eng
  • Alur, R., Etessami, K., Yannakakis, M., Inference of message sequence charts (2003) IEEE Trans. Software Eng, 29 (7), pp. 623-633. , July
  • Mauw, S., Reniers, M.A., High-level message sequence charts (1997) Proc. Int'l Conf. System Design Languages, pp. 291-306
  • Beer, I., Ben-David, S., Eisner, U., Rodeh, Y., Efficient detection of vacuity in ACTL formulas (1997) Lecture Notes In Computer Science, (1254), pp. 279-290. , Computer Aided Verification
  • D'Ippolito, N., Fishbein, D., Foster, H., Uchitel, S., Mtsa: Eclipse support for modal transition systems construction, analysis and elaboration (2007) Proc. OOPSLA Workshop Eclipse Technology Exchange, pp. 6-10
  • Van Ommering, R., Van Der Linden, F., Kramer, J., Magee, J., Koala component model for consumer electronics software (2000) Computer, 33 (3), pp. 78-85. , DOI 10.1109/2.825699
  • Damm, W., Harel, D., LSCs: Breathing life into message sequence charts (2001) Formal Methods in System Design, 19 (1), pp. 45-80. , DOI 10.1023/A:1011227529550
  • Magee, J., Pryce, N., Giannakopoulou, D., Kramer, J., Graphical animation of behavior models (2000) Proc. 22nd Int'l Conf. Software Eng, pp. 499-508
  • Kugler, H., Stern, M.J., Hubbard, E.J.A., Testing scenario- based models (2007) Proc. 10th Int'l Conf. Fundamental Approaches to Software Eng, pp. 306-320
  • Larsen, K., Xinxin, L., Equation solving using modal transition systems (1990) Proc. Fifth Ann IEEE Symp. Logic in Computer Science, pp. 108-117
  • Bontemps, Y., Schobbens, P.-Y., Loding, C., Synthesis of open reactive systems from scenario-based specifications (2004) Fundamenta Informaticae, 62 (2), pp. 139-169
  • Harel, D., Kugler, H., Synthesizing state-based object systems from lsc specifications (2002) Int'l J. Foundation of Computer Science, 13 (1), pp. 5-51
  • Krka, I., Brun, Y., Edwards, G., Medvidovic, N., Synthesizing partial component-level behavior models from system specifications (2009) Proc. Seventh Joint Meeting of the European Software Eng. Conf. and the, , ACM SIGSOFT Symp. Foundations of Software Eng
  • Pilone, D., Pitman, N., (2005) UML 2.0 in A Nutshell, , http://www.uml.org/2012, O'Reilly
  • Antonik, A., Huth, M., Larsen, K., Nyman, U., Wasowski, A., 20 years of modal and mixed specifications (2008) Bull. EATCS, 95, pp. 94-129. , June
  • Alrajeh, D., Kramer, J., Russo, A., Uchitel, S., Learning operational requirements from goal models (2009) Proc. 31st IEEE Int'l Conf. Software Eng, pp. 265-275

Citas:

---------- APA ----------
Sibay, G.E., Braberman, V., Uchitel, S. & Kramer, J. (2013) . Synthesizing modal transition systems from triggered scenarios. IEEE Transactions on Software Engineering, 39(7), 975-1001.
http://dx.doi.org/10.1109/TSE.2012.62
---------- CHICAGO ----------
Sibay, G.E., Braberman, V., Uchitel, S., Kramer, J. "Synthesizing modal transition systems from triggered scenarios" . IEEE Transactions on Software Engineering 39, no. 7 (2013) : 975-1001.
http://dx.doi.org/10.1109/TSE.2012.62
---------- MLA ----------
Sibay, G.E., Braberman, V., Uchitel, S., Kramer, J. "Synthesizing modal transition systems from triggered scenarios" . IEEE Transactions on Software Engineering, vol. 39, no. 7, 2013, pp. 975-1001.
http://dx.doi.org/10.1109/TSE.2012.62
---------- VANCOUVER ----------
Sibay, G.E., Braberman, V., Uchitel, S., Kramer, J. Synthesizing modal transition systems from triggered scenarios. IEEE Trans Software Eng. 2013;39(7):975-1001.
http://dx.doi.org/10.1109/TSE.2012.62