Artículo
Sibay, G.E.; Uchitel, S.; Braberman, V.; Kramer, J. "Distribution of modal transition systems" (2012) 18th International Symposium on Formal Methods, FM 2012. 7436 LNCS:403-417
Consulte la política de Acceso Abierto del editor
Abstract:
In order to capture all permissible implementations, partial models of component based systems are given as at the system level. However, iterative refinement by engineers is often more convenient at the component level. In this paper, we address the problem of decomposing partial behaviour models from a single monolithic model to a component-wise model. Specifically, given a Modal Transition System (MTS) M and component interfaces (the set of actions each component can control/monitor), can MTSs M 1 ..., M n matching the component interfaces be produced such that independent refinement of each M i will lead to a component Labelled Transition Systems (LTS) I i such that composing the I i s result in a system LTS that is a refinement of M? We show that a sound and complete distribution can be built when the MTS to be distributed is deterministic, transition modalities are consistent and the LTS determined by its possible transitions is distributable. © 2012 Springer-Verlag.
Registro:
| Documento: | Artículo |
| Título: | Distribution of modal transition systems |
| Autor: | Sibay, G.E.; Uchitel, S.; Braberman, V.; Kramer, J. |
| Ciudad: | Paris |
| Filiación: | Imperial College London, London, United Kingdom Universidad de Buenos Aires, FCEyN, Buenos Aires, Argentina |
| Palabras clave: | Distribution; Modal Transition Systems; Behaviour models; Component based systems; Component interfaces; Component levels; Componentwise; Distribution; Iterative refinement; Labelled transition systems; Modal Transition Systems; System levels; Artificial intelligence |
| Año: | 2012 |
| Volumen: | 7436 LNCS |
| Página de inicio: | 403 |
| Página de fin: | 417 |
| DOI: | http://dx.doi.org/10.1007/978-3-642-32759-9_33 |
| Título revista: | 18th International Symposium on Formal Methods, FM 2012 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7436LNCS_n_p403_Sibay |
Referencias:
- Beneš, N., Křetínský, J., Larsen, K.G., Srba, J., Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete (2009) LNCS, 5684, pp. 112-126. , Leucker, M., Morgan, C. (eds.) ICTAC 2009. Springer, Heidelberg
- Beneš, N., Ketínský, J., Larsen, K.G., Srba, J., On determinism in modal transition systems (2009) Theor. Comput. Sci., 410 (41), pp. 4026-4043
- Castellani, I., Mukund, M., Thiagarajan, P.S., Synthesizing Distributed Transition Systems from Global Specifications (1999) LNCS, 1738, pp. 219-231. , Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. Springer, Heidelberg
- D'Ippolito, N., Fishbein, D., Foster, H., Uchitel, S., MTSA: Eclipse support for modal transition systems construction, analysis and elaboration (2007) Eclipse 2007: Proceedings of the 2007 OOPSLA Workshop on Eclipse Technology Exchange, pp. 6-10. , ACM
- Fischbein, D., Brunet, G., D'Ippolito, N., Chechik, M., Uchitel, S., Weak alphabet merging of partial behaviour models (2011) TOSEM, pp. 1-49
- Godefroid, P., Piterman, N., Ltl generalized model checking revisited (2011) STTT, 13 (6), pp. 571-584
- Heljanko, K., Stefanescu, A., Complexity results for checking distributed implementability (2005) Proc. of the Fifth Int. Conf. on Application of Concurrency to System Design, pp. 78-87. , IEEE Computer Society Press
- Hopcroft, J.E., Ullman, J.D., (1979) Introduction to Automata Theory, Languages, and Computation, , Addison-Wesley
- Krka, I., Brun, Y., Edwards, G., Medvidovic, N., Synthesizing partial component-level behavior models from system specifications (2009) ESEC/FSE 2009, pp. 305-314. , ACM
- Larsen, K.G., Thomsen, B., A modal process logic (1988) LICS 1988, pp. 203-210. , IEEE Computer Society
- Milner, R., (1989) Communication and Concurrency, , Prentice-Hall, New York
- Magee, J., Kramer, J., (1999) Concurrency - State Models and Java Programs, , John Wiley
- Morin, R., Decompositions of Asynchronous Systems (1998) LNCS, 1466, pp. 549-564. , Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. Springer, Heidelberg
- Quinton, S., Graf, S., Contract-based verification of hierarchical systems of components (2008) SEFM 2008, pp. 377-381
- Stefanescu, A., (2006) Automatic Synthesis of Distributed Systems, , PhD thesis
- Stoll, M., (2005) MoTraS: A Tool for Modal Transition Systems, , Master's thesis, Technische Universitat Munchen, Fakultat fur Informatik (August)
- Sibay, G., Uchitel, S., Braberman, V., Existential live sequence charts revisited (2008) ICSE 2008, pp. 41-50
- Uchitel, S., Kramer, J., Magee, J., Incremental elaboration of scenario-based specifications and behaviour models using implied scenarios (2004) ACM TOSEM, 13 (1)A4 - Digiteo; AdaCore; SNCF; LEI; ENSTA ParisTech
Citas:
---------- APA ----------
Sibay, G.E., Uchitel, S., Braberman, V. & Kramer, J. (2012) . Distribution of modal transition systems. 18th International Symposium on Formal Methods, FM 2012, 7436 LNCS, 403-417.http://dx.doi.org/10.1007/978-3-642-32759-9_33
---------- CHICAGO ----------
Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J. "Distribution of modal transition systems" . 18th International Symposium on Formal Methods, FM 2012 7436 LNCS (2012) : 403-417.http://dx.doi.org/10.1007/978-3-642-32759-9_33
---------- MLA ----------
Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J. "Distribution of modal transition systems" . 18th International Symposium on Formal Methods, FM 2012, vol. 7436 LNCS, 2012, pp. 403-417.http://dx.doi.org/10.1007/978-3-642-32759-9_33
---------- VANCOUVER ----------
Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J. Distribution of modal transition systems. Lect. Notes Comput. Sci. 2012;7436 LNCS:403-417.http://dx.doi.org/10.1007/978-3-642-32759-9_33
