Navegar

Colección

Datos Estadísticas

Artículo

Fischbein, D.; Braberman, V.; Uchitel, S. "A Sound observational semantics for modal transition systems" (2009) 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009. 5684 LNCS:215-230
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:

Modal Transition Systems (MTS) are an extension of Labelled Transition Systems (LTS) that distinguish between required, proscribed and unknown behaviour and come equipped with a notion of refinement that supports incremental modelling where unknown behaviour is iteratively elaborated into required or proscribed behaviour. The original formulation of MTS introduces two alternative semantics for MTS, strong and weak, which require MTS models to have the same communicating alphabet, the latter allowing the use of a distinguished unobservable action. In this paper we show that the requirement of fixing the alphabet for MTS semantics and the treatment of observable actions are limiting if MTS are to support incremental elaboration of partial behaviour models. We present a novel semantics, branching alphabet semantics, for MTS inspired by branching LTS equivalence, we show that some unintuitive refinements allowed by weak semantics are avoided, and prove a number of theorems that relate branching refinement with alphabet refinement and consistency. These theorems, which do not hold for other semantics, support the argument for considering branching implementation of MTS as the basis for a sound semantics to support behaviour model elaboration. © 2009 Springer Berlin Heidelberg.

Registro:

Documento: Artículo
Título:A Sound observational semantics for modal transition systems
Autor:Fischbein, D.; Braberman, V.; Uchitel, S.
Ciudad:Kuala Lumpur
Filiación:Imperial College London, 180 Queen's Gate, London SW7 2RH, United Kingdom
University of Buenos Aires, C1428EGA, Argentina
Palabras clave:Behaviour models; Labelled transition systems; Modal Transition Systems; Observational semantics; Unobservable; Computer science; Laser tissue interaction; Semantics; Mathematical models
Año:2009
Volumen:5684 LNCS
Página de inicio:215
Página de fin:230
DOI: http://dx.doi.org/10.1007/978-3-642-03466-4_14
Título revista:6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5684LNCS_n_p215_Fischbein

Referencias:

  • Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A., Complexity of decision problems for mixed and modal specifications (2008) LNCS, 4962, pp. 112-126. , Amadio R.M. (ed.) FOSSACS 2008. Springer, Heidelberg
  • Brunet, G., (2006) A Characterization of Merging Partial Behavioural Models, , Master's thesis Univ. of Toronto (January)
  • Brunet, G., Chechik, M., Uchitel, S., Properties of behavioural model merging (2006) LNCS, 4085, pp. 98-114. , Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. Springer, Heidelberg
  • Cleaveland, R., Hennessy, M., Testing equivalence as a bisimulation equivalence (1993) Formal Asp. Comput., 5 (1), pp. 1-20
  • Dams, D., (1996) Abstract Interpretation and Partition Refinement for Model Checking, , PhD thesis Eindhoven University of Technology The Netherlands (July)
  • Fischbein, D., Uchitel, S., Behavioural model elaboration using mts (2007) Copenhagen Meeting on Modal Transition Systems
  • Fischbein, D., Uchitel, S., On correct and complete strong merging of partial behaviour models (2008) SIGSOFT 2008/ FSE-16, pp. 297-307. , ACM Press, New York
  • Fischbein, D., Uchitel, S., Braberman, V., A foundation for behavioural conformance in software product line architectures (2006) ROSATEA
  • Van Glabbeek, R., What is branching time semantics and why to use it? (1994) The Concurrency Column, pp. 190-198. , Nielsen, M. (ed.) Bulletin of the EATCS 53
  • Huth, M., Refinement is complete for implementations (2005) Formal Asp. Comput., 17 (2), pp. 113-137
  • Hüttel, H., Larsen, K.G., The use of static constructs in a modal process logic (1989) Logic at Botik, pp. 163-180
  • Jackson, M., (1995) Software Requirements & Specifications: A Lexicon of Practice, Principles and Prejudices, , ACM Press/Addison-Wesley Publishing Co
  • Keller, R.M., Formal verification of parallel programs (1976) Commun. ACM
  • Larsen, K., Xinxin, L., Equation solving using modal transition systems (1990) 5th Annual IEEE Symposium on Logic in Computer Science, pp. 108-117
  • Larsen, K.G., Steffen, B., Weise, C., A constraint oriented proof methodology based on modal transition systems (1995) LNCS, 1019. , Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. Springer, Heidelberg
  • Larsen, K.G., Thomsen, B., A modal process logic (1988) LICS
  • Milner, R., A modal characterisation of observable machine-behaviour (1981) LNCS, 112, pp. 25-34. , Astesiano, E., Böhm, C. (eds.) CAAP 1981. Springer, Heidelberg
  • Schneider, S., Schneider, S.A., (1999) Concurrent and Real Time Systems: The CSP Approach, , John Wiley & Sons Inc. New York
  • Uchitel, S., Chechik, M., Merging partial behavioural models (2004) SIGSOFT FSE, pp. 43-52. , Taylor, R.N., Dwyer, M.B. (eds.) ACM Press, New York
  • Uchitel, S., Kramer, J., Magee, J., Behaviour model elaboration using partial labelled transition systems (2003) ESEC/FSE 2003, pp. 19-27
  • Van Gabbeek, R.J., Weijland, W.P., Branching time and abstraction in bisimulation semantics (1996) J. ACM, 43 (3), pp. 555-600

Citas:

---------- APA ----------
Fischbein, D., Braberman, V. & Uchitel, S. (2009) . A Sound observational semantics for modal transition systems. 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009, 5684 LNCS, 215-230.
http://dx.doi.org/10.1007/978-3-642-03466-4_14
---------- CHICAGO ----------
Fischbein, D., Braberman, V., Uchitel, S. "A Sound observational semantics for modal transition systems" . 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009 5684 LNCS (2009) : 215-230.
http://dx.doi.org/10.1007/978-3-642-03466-4_14
---------- MLA ----------
Fischbein, D., Braberman, V., Uchitel, S. "A Sound observational semantics for modal transition systems" . 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009, vol. 5684 LNCS, 2009, pp. 215-230.
http://dx.doi.org/10.1007/978-3-642-03466-4_14
---------- VANCOUVER ----------
Fischbein, D., Braberman, V., Uchitel, S. A Sound observational semantics for modal transition systems. Lect. Notes Comput. Sci. 2009;5684 LNCS:215-230.
http://dx.doi.org/10.1007/978-3-642-03466-4_14