Algebraic Foundations

Algebraic foundations of system specification and design.

Foundational and methodological work is being done in the area of algebraic methods for system specification and design. Special interest areas have been the semantics of specification languages, specification design from informal requirements, modular specifications and specification of modules, and concepts for studying the correctness of refinement steps. Previous results of this research include the characterization of some notions concerning correctness of parameterized specifications and of abstract implementations, the study of behavioral semantics for algebraic specifications, and a formal framework for the stepwise development of specifications and programs. Some of these results have been applied to the semantic definition of the GLIDER (the specification language of the Esprit Project ICARUS) and, are also being applied to study the different aspects related to the development of modular and structured logic programs. Recent work in cooperation with the group of Prof. Ehrig at the T.U. Berlin includes the study of a paradigm for the integration of specification formalisms for the modelling and development of component-based systems, and the use of graph transformation systems as the basis for providing adequate semantics.

This research has been funded by the Spanish National Agency (Comision Asesora), the Catalan agency (CIRIT) and by some EC projects, such as ICARUS (co-financed also by the Spanish National Agency), COMPASS and MEDICIS.

Some recent publications in this area are:

M. Navarro, F. Orejas, A. Sanchez, On the Correctness of Modular Systems, Theoretical Comp. Science 140,1 (March, 1995), pp. 139-178. ©Elsevier Science Inc.
R. Jimenez, F. Orejas, H. Ehrig, Compositionality and Compatibility of Parameterization and Parameter Passing in Specification Languages, Math. Structures in Computer Science, 5, Cambridge Univ. Press (1995), pp. 283 -313. ©Cambridge University Press
F. Orejas, M. Navarro, A. Sanchez, Algebraic Implementation of Abstract Data Types: a survey of concepts and new compositionality results, Mathematical Structures in Computer Science, 6 Cambridge Univ. Press (1996) pp. 33 - 67. ©Cambridge University Press
E. Dubois, J. Hagelstein, A. Van Lamsweerde, F. Orejas, J. Souquieres, P. Wodon, A guided tour through ICARUS, ACM Software Engineering Notes, 20 (1995) pp. 28 - 33.
F. Orejas, E. Pino, H. Ehrig, Institutions for Logic Programming, Theoretical Computer Science, 173 (1997) pp. 485 - 511. ©Elsevier Science Inc.
S. Clerici, R. Jimenez, F. Orejas, Class-Sort Polymorphism in Glider, in Recent trends in data type specification (M. Haveraaen, O. Owe, O.J. Dahl, eds.), Springer-Verlag Lecture Notes in Computer Science 1130 (1996) pp. 143 - 160.©Springer-Verlag LNCS.
H. Ehrig., F. Orejas, Integration paradigm for data type and process specification techniques, Bull. EATCS 60, 1998, pp. 90-97.
H. Ehrig, R. Heckel, M. Llabres, F. Orejas, J. Padberg, G. Rozenberg, Double-pullback graph transitions: a rule-based framework with incomplete information, in Proc. Theory and Applications of Graph Transformation, Springer-Verlag Lecture Notes in Computer Science 1764 (1999), pp. 85-102 ©Springer-Verlag LNCS.
P. Lucio, F. Orejas, E. Pino, An algebraic framework for the definition of compositional semantics of normal logic programs, J. of Logic Programming 40(1), (1999) pp. 89-124.©Elsevier Science Inc.
F. Cornelius, M. Baldamus, H. Ehrig, F. Orejas, Abstract and behaviour module specifications, Mathematical Structures in Computer Science, 9 Cambridge Univ. Press (1999) pp. 21- 62. ©Cambridge University Press
F. Orejas, Chapter 6: Structuring and Modularity, in Algebraic Foundations of System Specification, E. Astesiano, E., H.-J. Kreowski, B. Krieg-Brückner (eds), Springer-Verlag 1999, pp. 159-200.©Springer-Verlag
An algebraic framework for higher-order modules, R. Jimenez, F. Orejas. In Proc. FM'99, Toulouse, Springer-Verlag Lecture Notes in Computer Science 1709, (1999) pp. 1778-1796©Springer-Verlag LNCS.
F. Orejas, E. Pino, Semantic definitions for normal open programs, in Proc. Int. Conf. on Logic Programming, Las Cruces (USA) (1999), pp. 200-214.©M.I.T.
F. Orejas, E. Pino, A general algebraic framework for studying modular systems, in Recent Trends in Algebraic Development Techniques (D. Bert, C. Choppy, P. Mosses, eds.) Springer-Verlag Lecture Notes in Computer Science 1827 (2000) pp. 271 - 290. ©Springer-Verlag LNCS.
R. Heckel, M. Llabres, H. Ehrig, F. Orejas: Concurrency and loose semantics of open graph transformation systems, to appear in Math. Structures in Comp. Sc.
F. Orejas, E. Pino, E. Pasarella, Semantics of Normal Logic Programs with embedded implications, to appear in Proc. Int. Conf. on Logic Programming, (2001)
F. Orejas, H. Ehrig, E. Pino, Tight and Loose Semantics for Transformation Systems, presented at WADT 2001, Genova.