Heterogeniczne środowiska logiczne - spojrzenie instytucyjne

Speaker(s)

prof. Andrzej Tarlecki

Affiliation

Uniwersytet Warszawski

Date

March 16, 2009, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

HETEROGENEOUS LOGICAL ENVIRONMENTS: AN INSTITUTIONAL VIEW We work within the theory of institutions as a framework where the theory of specification and formal software development may be presented in an adequately general and abstract way. As different logical systems may be appropriate or most convenient for specification of different modules of the same system, of different aspects of system behaviour, or of different stages of system development, we need a number of logical systems to be used in the same specification and development project. This motivates the presented research on heterogeneous logical environments and specifications built in such environments. We formalise logical systems as institutions. To enable a sensible use of a number of institutions together, in heterogeneous logical environments we link them with each other by institution morphisms or other maps between institutions, like institution comorphisms. Using them together with other standard (intra-institutional) specification-building operations, one builds heterogeneous structured specifications, which may involve a number of institutions to specify some aspects or some parts of the system, but ultimately focus at one institution of interest. One family of logical systems is suggested by UML, where system specifications typically involve a number of diagrams of different kinds, each capturing a different aspect of the system. Each kind of UML diagrams leads to a separate logical system which, at least in principle, can be formalised as an institution. Expected relationships between system properties specified by different kinds of UML diagrams may now be captured using appropriate institution maps. UML specifications, however, are quite different from focused heterogeneous specifications mentioned above. They just form a collection of specifications residing in different institutions of UML diagrams. We present a general abstract concept of a distributed heterogeneous specifcations that consist of a collection of specifications focused at various institutions in an underlying heterogeneous logical environment, linked by specification morphisms generalised by involving institution maps. Distributed heterogeneous specifications come equipped with a rather natural semantics, given in terms of compatible families of models of component specifications. This yields in the standard way a number of usual concepts: consistency, semantic consequence, and perhaps most importantly, implementation of one distributed specification by another. Each basic concept of a map between institutions can be captured by institution (co)morphisms --- as a span of (co)morphisms. Replacing a map between institutions by an appropriate span of (co)morphisms allows one to represent exactly the same relationship between institutions and their components. However, the categories of specifications that emerge in each case are different. Nevertheless, we argue that the expressive power of distributed specicfications built over them does not essentially differ.

---