Andrzej Tarlecki: Software Specification and Development in Heterogeneous Environments

The overall idea of the talk is to present recent work aimed at dealing with multiple logical systems in a single specification and software development task. I first recall the basic technical notions related to modelling logical systems as institutions, presenting them using (model-theoretic) parchments, relating institutions and parchments using morphisms of various kinds, etc. Given this background, I discuss in some detail the possibilities for combining logical systems using standard categorical constructions in the category of either institutions or parchments. Some positive results (like completeness of the relevant categories) are given. However, these do not lead to miraculous combinations of any possible logical features, but rather provide a framework which limits the necessary ingenuity (and human decisions) to some specific points, and hint at possible techniques of formulating the necessary decisions in the most effective way. Then, I sketch how the mechanisms of various mappings between institutions may be used to cater for heterogeneous specifications, which span an number of linked institutions, and for the description of the development process which may 'migrate' between various institutions in the course of development of separate modules of the system. Overall, a picture of a heterogeneous logical environment for software specification and development is emerging as as simply a diagram of institutions linked by morphisms of various kinds.
Last modified: Mon Sep 26 12:51:06 CEST 2005