Revisiting compatibility of input-output modal transition systems
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, interfac...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Springer Verlag
2014
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 06495caa a22007337a 4500 | ||
|---|---|---|---|
| 001 | PAPER-14743 | ||
| 003 | AR-BaUEN | ||
| 005 | 20251211113920.0 | ||
| 008 | 190411s2014 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84958552959 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Krka, I. | |
| 245 | 1 | 0 | |a Revisiting compatibility of input-output modal transition systems |
| 260 | |b Springer Verlag |c 2014 | ||
| 504 | |a De Alfaro, L., Henzinger, T.A., Interface automata (2001) ESEC/FSE | ||
| 504 | |a 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 | ||
| 504 | |a 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) | ||
| 504 | |a 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 | ||
| 504 | |a Fischbein, D., D'Ippolito, N., Brunet, G., Chechik, M., Uchitel, S., Weak alphabet merging of partial behaviour models (2012) ACM TOSEM, 21 (2) | ||
| 504 | |a Fischbein, D., Uchitel, S., On correct and complete strong merging of partial behaviour models (2008) FSE | ||
| 504 | |a Harel, D., Statecharts: A visual formalism for complex systems (1987) Sci. of Comp. Prog. | ||
| 504 | |a Keller, R.M., Formal verification of parallel programs (1976) Com. of the ACM | ||
| 504 | |a Krka, I., Brun, Y., Edwards, G., Medvidovic, N., Synthesizing partial component-level behavior models from system specifications (2009) ESEC/FSE | ||
| 504 | |a Krka, I., Medvidovic, N., Revisiting modal interface automata (2012) FORMSERA | ||
| 504 | |a Krka, I., Medvidovic, N., Distributing refinements of a system-level partial behavior model (2013) RE | ||
| 504 | |a Krka, I., Medvidovic, N., Component-aware triggered scenarios WICSA, , Submitted | ||
| 504 | |a 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 | ||
| 504 | |a Larsen, K.G., Thomsen, B., A modal process logic (1988) LICS | ||
| 504 | |a Larsen, K.G., Xinxin, L., Equation solving using modal transition systems (1990) LICS | ||
| 504 | |a Lynch, N.A., Tuttle, M.R., Hierarchical correctness proofs for distributed algorithms (1987) PODC 1987 | ||
| 504 | |a Magee, J., Kramer, J., (2006) Concurrency: State Models & Java Programs | ||
| 504 | |a Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R., Modal interfaces: Unifying interface automata and modal specifications (2009) EMSOFT | ||
| 504 | |a Sibay, G.E., Braberman, V.A., Uchitel, S., Kramer, J., Synthesising modal transition systems from triggered scenarios (2013) IEEE TSE | ||
| 504 | |a 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 | ||
| 504 | |a Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) IEEE TSE, 35 (3)A4 - | ||
| 506 | |2 openaire |e Política editorial | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Google Inc, Zürich, Switzerland | ||
| 593 | |a Computing Department, Imperial College London, London, United Kingdom | ||
| 593 | |a Departamento de Computatión, FCEyN, Universidad de Buenos Aires, Argentina | ||
| 593 | |a University of Southern California, Los Angeles CA, United States | ||
| 690 | 1 | 0 | |a INTERFACE STATES |
| 690 | 1 | 0 | |a AUTOMATA-BASED FORMALISMS |
| 690 | 1 | 0 | |a COMPONENT IMPLEMENTATIONS |
| 690 | 1 | 0 | |a EXTERNAL BEHAVIOR |
| 690 | 1 | 0 | |a INTERFACE AUTOMATA |
| 690 | 1 | 0 | |a MODAL TRANSITION SYSTEMS |
| 690 | 1 | 0 | |a MODELING FORMALISMS |
| 690 | 1 | 0 | |a REQUIREMENTS SPECIFICATIONS |
| 690 | 1 | 0 | |a SOFTWARE SYSTEMS |
| 690 | 1 | 0 | |a AUTOMATA THEORY |
| 700 | 1 | |a D'Ippolito, N. | |
| 700 | 1 | |a Medvidović, N. | |
| 700 | 1 | |a Uchitel, Sebastián | |
| 711 | 2 | |c Singapore |d 12 May 2014 through 16 May 2014 |g Código de la conferencia: 105001 | |
| 773 | 0 | |d Springer Verlag, 2014 |g v. 8442 LNCS |h pp. 367-381 |p Lect. Notes Comput. Sci. |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |x 03029743 |w (AR-BaUEN)CENRE-983 |z 9783319064093 |t 19th International Symposium on Formal Methods, FM 2014 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84958552959&doi=10.1007%2f978-3-319-06410-9_26&partnerID=40&md5=2cd423fe4e409d9578c3f4a39767cfca |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1007/978-3-319-06410-9_26 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_03029743_v8442LNCS_n_p367_Krka |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8442LNCS_n_p367_Krka |y Registro en la Biblioteca Digital |
| 961 | |a paper_03029743_v8442LNCS_n_p367_Krka |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 963 | |a VARI | ||
| 999 | |c 75696 | ||