Navegar

Colección

Datos Estadísticas

Artículo

Krka, I.; D'Ippolito, N.; Medvidović, N.; Uchitel, S. "Revisiting compatibility of input-output modal transition systems" (2014) 19th International Symposium on Formal Methods, FM 2014. 8442 LNCS:367-381
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Modern software systems are typically built of components that communicate through their external interfaces. The external behavior of a component can be effectively described using finite state automata-based formalisms. Such component models can then used for varied analyses. For example, interface automata, which model the behavior of components in terms of component states and transitions between them, can be used to check whether the resulting system is compatible. By contrast, partial-behavior modeling formalisms, such as modal transition systems, can be used to capture and then verify properties of sets of prospective component implementations that satisfy an incomplete requirements specification. In this paper, we study how pairwise compatibility should be defined for partial-behavior models. To this end, we describe the limitations of the existing compatibility definitions, propose a set of novel compatibility notions for modal interface automata, and propose efficient, correct, and complete compatibility checking procedures © 2014 Springer International Publishing Switzerland.

Registro:

Documento: Artículo
Título:Revisiting compatibility of input-output modal transition systems
Autor:Krka, I.; D'Ippolito, N.; Medvidović, N.; Uchitel, S.
Ciudad:Singapore
Filiación:Google Inc, Zürich, Switzerland
Computing Department, Imperial College London, London, United Kingdom
Departamento de Computatión, FCEyN, Universidad de Buenos Aires, Argentina
University of Southern California, Los Angeles CA, United States
Palabras clave:Interface states; Automata-based formalisms; Component implementations; External behavior; Interface automata; Modal Transition Systems; Modeling formalisms; Requirements specifications; Software systems; Automata theory
Año:2014
Volumen:8442 LNCS
Página de inicio:367
Página de fin:381
DOI: http://dx.doi.org/10.1007/978-3-319-06410-9_26
Título revista:19th International Symposium on Formal Methods, FM 2014
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8442LNCS_n_p367_Krka

Referencias:

  • De Alfaro, L., Henzinger, T.A., Interface automata (2001) ESEC/FSE
  • Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R., On weak modal compatibility, refinement, and the mio workbench (2010) TACAS 2010. LNCS, 6015, pp. 175-189. , Esparza, J., Majumdar, R. (eds.), Springer, Heidelberg
  • Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J., (2012) Featured Transition Systems: Foundations for Verifying Variability-intensive Systems and Their Application to LTL Model Checking, 39 (8)
  • D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., The modal transition system control problem (2012) FM 2012. LNCS, 7436, pp. 155-170. , Giannakopoulou, D., Mery, D. (eds.), Springer, Heidelberg
  • Fischbein, D., D'Ippolito, N., Brunet, G., Chechik, M., Uchitel, S., Weak alphabet merging of partial behaviour models (2012) ACM TOSEM, 21 (2)
  • Fischbein, D., Uchitel, S., On correct and complete strong merging of partial behaviour models (2008) FSE
  • Harel, D., Statecharts: A visual formalism for complex systems (1987) Sci. of Comp. Prog.
  • Keller, R.M., Formal verification of parallel programs (1976) Com. of the ACM
  • Krka, I., Brun, Y., Edwards, G., Medvidovic, N., Synthesizing partial component-level behavior models from system specifications (2009) ESEC/FSE
  • Krka, I., Medvidovic, N., Revisiting modal interface automata (2012) FORMSERA
  • Krka, I., Medvidovic, N., Distributing refinements of a system-level partial behavior model (2013) RE
  • Krka, I., Medvidovic, N., Component-aware triggered scenarios WICSA, , Submitted
  • Larsen, K.G., Nyman, U., Wsowski, a.: Modal i/o automata for interface and product line theories (2007) ESOP 2007. LNCS, 4421, pp. 64-79. , De Nicola, R. (ed.), Springer, Heidelberg
  • Larsen, K.G., Thomsen, B., A modal process logic (1988) LICS
  • Larsen, K.G., Xinxin, L., Equation solving using modal transition systems (1990) LICS
  • Lynch, N.A., Tuttle, M.R., Hierarchical correctness proofs for distributed algorithms (1987) PODC 1987
  • Magee, J., Kramer, J., (2006) Concurrency: State Models & Java Programs
  • Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R., Modal interfaces: Unifying interface automata and modal specifications (2009) EMSOFT
  • Sibay, G.E., Braberman, V.A., Uchitel, S., Kramer, J., Synthesising modal transition systems from triggered scenarios (2013) IEEE TSE
  • Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J., Distribution of modal transition systems (2012) FM 2012. LNCS, 7436, pp. 403-417. , Giannakopoulou, D., Mery, D. (eds.), Springer, Heidelberg
  • Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) IEEE TSE, 35 (3)A4 -

Citas:

---------- APA ----------
Krka, I., D'Ippolito, N., Medvidović, N. & Uchitel, S. (2014) . Revisiting compatibility of input-output modal transition systems. 19th International Symposium on Formal Methods, FM 2014, 8442 LNCS, 367-381.
http://dx.doi.org/10.1007/978-3-319-06410-9_26
---------- CHICAGO ----------
Krka, I., D'Ippolito, N., Medvidović, N., Uchitel, S. "Revisiting compatibility of input-output modal transition systems" . 19th International Symposium on Formal Methods, FM 2014 8442 LNCS (2014) : 367-381.
http://dx.doi.org/10.1007/978-3-319-06410-9_26
---------- MLA ----------
Krka, I., D'Ippolito, N., Medvidović, N., Uchitel, S. "Revisiting compatibility of input-output modal transition systems" . 19th International Symposium on Formal Methods, FM 2014, vol. 8442 LNCS, 2014, pp. 367-381.
http://dx.doi.org/10.1007/978-3-319-06410-9_26
---------- VANCOUVER ----------
Krka, I., D'Ippolito, N., Medvidović, N., Uchitel, S. Revisiting compatibility of input-output modal transition systems. Lect. Notes Comput. Sci. 2014;8442 LNCS:367-381.
http://dx.doi.org/10.1007/978-3-319-06410-9_26