Heterogeniczne środowiska logiczne - spojrzenie instytucyjne
- Prelegent(ci)
- prof. Andrzej Tarlecki
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 16 marca 2009 10:15
- Pokój
- p. 4790
- Seminarium
- Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
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.