Navegar

Colección

Datos Estadísticas

Artículo

Castro, P.F.; Aguirre, N.; Pombo, C.L.; Maibaum, T.S.E. "Categorical foundations for structured specifications in Z" (2015) Formal Aspects of Computing. 27(5-6):831-865
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:

In this paper we present a formalization of the Z notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of Z and its related concepts. We show that the main structuring mechanisms of Z are captured smoothly by categorical constructions. In particular, we provide a straightforward and clear semantics for promotion, a powerful structuring technique that is often not presented as part of the schema calculus. Here we show that promotion is already an operation over schemas (and more generally over specifications), that allows one to promote schemas that operate on a local notion of state to operate on a subsuming global state, and in particular can be used to conveniently define large specifications from collections of simpler ones. Moreover, our proposed formalization facilitates the combination of Z with other notations in order to produce heterogeneous specifications, i.e., specifications that are obtained by using various different mathematical formalisms. Thus, our abstract and precise formulation of Z is useful for relating this notation with other formal languages used by the formal methods community. We illustrate this by means of a known combination of formal languages, namely the combination of Z with CSP. © 2015, British Computer Society.

Registro:

Documento: Artículo
Título:Categorical foundations for structured specifications in Z
Autor:Castro, P.F.; Aguirre, N.; Pombo, C.L.; Maibaum, T.S.E.
Filiación:Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, Río Cuarto, Córdoba, 5800, Argentina
Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina
Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Buenos Aires, Argentina
Department of Computing and Software, McMaster University, Hamilton, ON, Canada
Palabras clave:Category theory; Heterogeneous specifications; System specification; System verification; Z Notation; Calculations; Computational linguistics; Computer hardware description languages; Formal languages; Formal methods; Formal specification; Semantics; Category theory; Formal framework; Mathematical formalism; Structured specification; Structuring mechanisms; System specification; System verifications; Z notation; Specifications
Año:2015
Volumen:27
Número:5-6
Página de inicio:831
Página de fin:865
DOI: http://dx.doi.org/10.1007/s00165-015-0336-0
Título revista:Formal Aspects of Computing
Título revista abreviado:Formal Aspects Comput
ISSN:09345043
CODEN:FACME
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09345043_v27_n5-6_p831_Castro

Referencias:

  • Baar, T., Strohmeier, A., Moreira, A., Mellor, S., UML 2004 (2004) Lecture notes in computer science, 3273. , Springer, Berlin
  • Barr, M., Wells, C., Category theory for computer science (1999) In, , Centre de Recherches Mathématiques, Université de Montréal
  • Baumeister, H., Relating abstract datatypes and Z-schemata (1999) Proc. of WADT ’99. Lecture notes in computer science, 1827, pp. 366-382. , Springer, Berlin
  • Bérnabou, J., Introduction to bicategories (1967) Complementary definitions of programming language semantics. LNM, 42, pp. 1-77. , Springer, Berlin
  • Borzyszkowski, T., Higher-order logic and theorem proving for structured specifications (1999) Proc. of WADT ’99. Lecture notes in computer science, 1827. , Springer, Berlin
  • Brien, S.M., Martin, A.P., A calculus for schemas in Z (2000) J Symb Comput, 30 (1), pp. 63-91
  • Bujorianu, M.C., Integration of specification languages using viewpoints (2004) Proc. of IFM ’04. Lecture notes in computer science, 2999. , Springer, Berlin
  • Castro, P.F., Aguirre, N., Lopez Pombo, C.G., Maibaum, T.S.E., A categorical approach to structuring and promoting Z specifications (2012) Proc. of FACS’12. Lecture notes in computer science, 7684. , Springer, Berlin
  • Chang, C.C., Keisler, H.J., (1990) Model theory, , North Holland: NY
  • Diaconescu, R., (2008) Institution-independent model theory, , Birkhäuser Verlag, Basel
  • Enderton, H., (2001) A mathematical introduction to logic, , Academic Press, Dublin
  • Fiadeiro, J., (2004) Categories for software engineering, , Springer, Berlin
  • Fiadeiro, J., Maibaum, T.S.E., Temporal theories as modularisation units for concurrent system specification (1992) Form Asp Comput, 4 (3), pp. 239-272
  • Finkelstein, A., Kramer, J., Nuseibeh, B., Finkelstein, L., Goedicke, M., Viewpoints: a framework for integrating multiple perspectives in system development (1992) Int J Softw Eng Knowl Eng, 2 (1), pp. 31-57
  • Fischer, C., (1997) Combining CSP and Z, , Technical Report: University of Oldenburg
  • Goguen, J., Burstall, R., Institutions: abstract model theory for specification and programming (1992) J ACM, 39 (1), pp. 95-146
  • Henson, M., Reeves, S., Revising Z: part I—logic and semantics (1999) Form Asp Comput, 11 (4), pp. 359-380
  • Henson, M., Reeves, S., Revising Z: part II—logical development (1999) Form Asp Comput, 11 (4), pp. 381-401
  • Hoare, C.A.R., Jifeng, H., Unifying theories of programming (1998), Prentice Hall College Division, Englewood Cliffs; Jacky, J., (1997) The way of Z, practical programming with formal methods, , Cambridge University Press, Cambridge
  • Lano, K., Model-driven software development with UML and java (2009) Course Technology
  • MacLane, S., (1998) Categories for the working mathematician, , Springer, Berlin
  • Meyer, B., (2000) Object-oriented software construction, , Prentice Hall, Englewood Cliffs
  • Mossakowski, T., Maeder, C., Lüttich, K., The heterogeneous tool set (hets). In: Proc (2007) of 4th international verification workshop in connection with CADE-21, , http://CEUR-WS.org
  • Nicholls, J., Z notation: version 1.2 (1995) Z standards panel
  • Mossakowski, T., Pawlowski, T.A., Combining and representing logical systems (1997) Proc. of category theory and computer science’97. Lecture notes in computer science, 1290. , Springer, Berlin
  • Mossakowski, T., Roggenbach, M., Structured CSP—a process algebra as an institution (2006) Proc. of WADT’06. Lecture notes in computer science, 4409. , Springer, Berlin
  • Oliveira, M., Cavalcanti, A., Woodcock, J., A UTP semantics for circus (2009) Form Asp Comput, 21 (2), pp. 3-32
  • Parnas, D., On the criteria to be used in decomposing systems into modules (1972) Commun. ACM, 15 (12), pp. 1053-1058
  • Parnas, D., The modular structure of complex system (1985) IEEE Trans Softw Eng, 11 (3), pp. 259-266
  • Risk! Rules of Play (1963) Parker Brothers; Spivey, J.M., Towards a formal semantics for the Z notation. Oxford University Computing Laboratory, T.M (1984) PRG-41
  • Spivey, J.M., Understanding Z: a specification language and its formal semantics (1988) Cambridge Tracts in Theoretical Computer Science
  • Spivey, J.M., The Z notation: a reference manual (1992), Prentice Hall, Englewood Cliffs; Tarlecki, A., Moving between logical systems (1995) Proc. of ADT/COMPASS’95. Lecture notes in computer science, 1130. , Springer, Berlin
  • Webber, M., Combining statecharts and Z for the design of safety-critical control systems (1996) Proc. of FME’96. Lecture notes in computer science, 1051. , Springer, Berlin
  • Woodcock, J., Mathematics as a management tool: proof rules for promotion (1990) In: Software engineering for large software systems, , Springer, Netherlands
  • Woodcock, J., Davies, J., (1996) Using Z: specification, refinement, and proof, , Prentice Hall, Englewood Cliffs
  • Woodcock, J., Cavancanti, A., Circus: a concurrent refinement language (2001) Technical report, , Oxford University Computing Laboratory, Oxford, UK

Citas:

---------- APA ----------
Castro, P.F., Aguirre, N., Pombo, C.L. & Maibaum, T.S.E. (2015) . Categorical foundations for structured specifications in Z. Formal Aspects of Computing, 27(5-6), 831-865.
http://dx.doi.org/10.1007/s00165-015-0336-0
---------- CHICAGO ----------
Castro, P.F., Aguirre, N., Pombo, C.L., Maibaum, T.S.E. "Categorical foundations for structured specifications in Z" . Formal Aspects of Computing 27, no. 5-6 (2015) : 831-865.
http://dx.doi.org/10.1007/s00165-015-0336-0
---------- MLA ----------
Castro, P.F., Aguirre, N., Pombo, C.L., Maibaum, T.S.E. "Categorical foundations for structured specifications in Z" . Formal Aspects of Computing, vol. 27, no. 5-6, 2015, pp. 831-865.
http://dx.doi.org/10.1007/s00165-015-0336-0
---------- VANCOUVER ----------
Castro, P.F., Aguirre, N., Pombo, C.L., Maibaum, T.S.E. Categorical foundations for structured specifications in Z. Formal Aspects Comput. 2015;27(5-6):831-865.
http://dx.doi.org/10.1007/s00165-015-0336-0