Categorical foundations for structured specifications in Z
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...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , |
| Formato: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Springer-Verlag London Ltd
2015
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 09697caa a22010457a 4500 | ||
|---|---|---|---|
| 001 | PAPER-13176 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204327.0 | ||
| 008 | 190411s2015 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84947613166 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a FACME | ||
| 100 | 1 | |a Castro, P.F. | |
| 245 | 1 | 0 | |a Categorical foundations for structured specifications in Z |
| 260 | |b Springer-Verlag London Ltd |c 2015 | ||
| 270 | 1 | 0 | |m Castro, P.F.; Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, Argentina; email: pcastro@dc.exa.unrc.edu.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Baar, T., Strohmeier, A., Moreira, A., Mellor, S., UML 2004 (2004) Lecture notes in computer science, 3273. , Springer, Berlin | ||
| 504 | |a Barr, M., Wells, C., Category theory for computer science (1999) In, , Centre de Recherches Mathématiques, Université de Montréal | ||
| 504 | |a Baumeister, H., Relating abstract datatypes and Z-schemata (1999) Proc. of WADT ’99. Lecture notes in computer science, 1827, pp. 366-382. , Springer, Berlin | ||
| 504 | |a Bérnabou, J., Introduction to bicategories (1967) Complementary definitions of programming language semantics. LNM, 42, pp. 1-77. , Springer, Berlin | ||
| 504 | |a Borzyszkowski, T., Higher-order logic and theorem proving for structured specifications (1999) Proc. of WADT ’99. Lecture notes in computer science, 1827. , Springer, Berlin | ||
| 504 | |a Brien, S.M., Martin, A.P., A calculus for schemas in Z (2000) J Symb Comput, 30 (1), pp. 63-91 | ||
| 504 | |a Bujorianu, M.C., Integration of specification languages using viewpoints (2004) Proc. of IFM ’04. Lecture notes in computer science, 2999. , Springer, Berlin | ||
| 504 | |a 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 | ||
| 504 | |a Chang, C.C., Keisler, H.J., (1990) Model theory, , North Holland: NY | ||
| 504 | |a Diaconescu, R., (2008) Institution-independent model theory, , Birkhäuser Verlag, Basel | ||
| 504 | |a Enderton, H., (2001) A mathematical introduction to logic, , Academic Press, Dublin | ||
| 504 | |a Fiadeiro, J., (2004) Categories for software engineering, , Springer, Berlin | ||
| 504 | |a Fiadeiro, J., Maibaum, T.S.E., Temporal theories as modularisation units for concurrent system specification (1992) Form Asp Comput, 4 (3), pp. 239-272 | ||
| 504 | |a 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 | ||
| 504 | |a Fischer, C., (1997) Combining CSP and Z, , Technical Report: University of Oldenburg | ||
| 504 | |a Goguen, J., Burstall, R., Institutions: abstract model theory for specification and programming (1992) J ACM, 39 (1), pp. 95-146 | ||
| 504 | |a Henson, M., Reeves, S., Revising Z: part I—logic and semantics (1999) Form Asp Comput, 11 (4), pp. 359-380 | ||
| 504 | |a Henson, M., Reeves, S., Revising Z: part II—logical development (1999) Form Asp Comput, 11 (4), pp. 381-401 | ||
| 504 | |a 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 | ||
| 504 | |a Lano, K., Model-driven software development with UML and java (2009) Course Technology | ||
| 504 | |a MacLane, S., (1998) Categories for the working mathematician, , Springer, Berlin | ||
| 504 | |a Meyer, B., (2000) Object-oriented software construction, , Prentice Hall, Englewood Cliffs | ||
| 504 | |a 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 | ||
| 504 | |a Nicholls, J., Z notation: version 1.2 (1995) Z standards panel | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Oliveira, M., Cavalcanti, A., Woodcock, J., A UTP semantics for circus (2009) Form Asp Comput, 21 (2), pp. 3-32 | ||
| 504 | |a Parnas, D., On the criteria to be used in decomposing systems into modules (1972) Commun. ACM, 15 (12), pp. 1053-1058 | ||
| 504 | |a Parnas, D., The modular structure of complex system (1985) IEEE Trans Softw Eng, 11 (3), pp. 259-266 | ||
| 504 | |a 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 | ||
| 504 | |a Spivey, J.M., Understanding Z: a specification language and its formal semantics (1988) Cambridge Tracts in Theoretical Computer Science | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Woodcock, J., Mathematics as a management tool: proof rules for promotion (1990) In: Software engineering for large software systems, , Springer, Netherlands | ||
| 504 | |a Woodcock, J., Davies, J., (1996) Using Z: specification, refinement, and proof, , Prentice Hall, Englewood Cliffs | ||
| 504 | |a Woodcock, J., Cavancanti, A., Circus: a concurrent refinement language (2001) Technical report, , Oxford University Computing Laboratory, Oxford, UK | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, Río Cuarto, Córdoba, 5800, Argentina | ||
| 593 | |a Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina | ||
| 593 | |a Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Buenos Aires, Argentina | ||
| 593 | |a Department of Computing and Software, McMaster University, Hamilton, ON, Canada | ||
| 690 | 1 | 0 | |a CATEGORY THEORY |
| 690 | 1 | 0 | |a HETEROGENEOUS SPECIFICATIONS |
| 690 | 1 | 0 | |a SYSTEM SPECIFICATION |
| 690 | 1 | 0 | |a SYSTEM VERIFICATION |
| 690 | 1 | 0 | |a Z NOTATION |
| 690 | 1 | 0 | |a CALCULATIONS |
| 690 | 1 | 0 | |a COMPUTATIONAL LINGUISTICS |
| 690 | 1 | 0 | |a COMPUTER HARDWARE DESCRIPTION LANGUAGES |
| 690 | 1 | 0 | |a FORMAL LANGUAGES |
| 690 | 1 | 0 | |a FORMAL METHODS |
| 690 | 1 | 0 | |a FORMAL SPECIFICATION |
| 690 | 1 | 0 | |a SEMANTICS |
| 690 | 1 | 0 | |a CATEGORY THEORY |
| 690 | 1 | 0 | |a FORMAL FRAMEWORK |
| 690 | 1 | 0 | |a MATHEMATICAL FORMALISM |
| 690 | 1 | 0 | |a STRUCTURED SPECIFICATION |
| 690 | 1 | 0 | |a STRUCTURING MECHANISMS |
| 690 | 1 | 0 | |a SYSTEM SPECIFICATION |
| 690 | 1 | 0 | |a SYSTEM VERIFICATIONS |
| 690 | 1 | 0 | |a Z NOTATION |
| 690 | 1 | 0 | |a SPECIFICATIONS |
| 700 | 1 | |a Aguirre, N. | |
| 700 | 1 | |a Pombo, C.L. | |
| 700 | 1 | |a Maibaum, T.S.E. | |
| 773 | 0 | |d Springer-Verlag London Ltd, 2015 |g v. 27 |h pp. 831-865 |k n. 5-6 |p Formal Aspects Comput |x 09345043 |t Formal Aspects of Computing | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84947613166&doi=10.1007%2fs00165-015-0336-0&partnerID=40&md5=3a9f18e3eaa4d004b0d6588e50155c8c |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-015-0336-0 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_09345043_v27_n5-6_p831_Castro |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_09345043_v27_n5-6_p831_Castro |y Registro en la Biblioteca Digital |
| 961 | |a paper_09345043_v27_n5-6_p831_Castro |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 74129 | ||