3 Comparison With Related Work

  One of the most important objectives we have for attending the workshop is to find out more about related work. We have seen little other work addressing the general question of semantic spaces for general system artifacts, or seeking an integrated formal treatment of the mathematical modeling of physical systems and the semantics of symbolic representations for physical systems and software systems. The closest thing we know of is a body of work in artificial intelligence called functional representation [Cha94]. This work explores understanding of ``causal processes'' and ``device behavior'', where a ``device'' might involve physical hardware or software or both. It has influenced our thinking by emphasizing the significance of an integrated mathematical modeling framework that deals with not just software systems but the physical systems in which they are embedded. In fact, a recent paper describes a ``smallest ontological framework'' [CJ96] which (except for vocabulary) is consistent with our starting point in Figure 1. However, though specifications and templates (by other names, of course) are central issues there, too, the functional representation community has concentrated on the structure of $\mathcal{B}$ and languages for $\mathcal{C}$. So we view our present contribution as complementary and orthogonal.

Most work on integrating formal specifications into the software life-cycle relies on using one language for writing specifications (e.g., Larch or $\mathcal{Z}$) and another language for writing implementations (e.g., Ada or C++) [KH96]. We have concentrated on a single integrated language (RESOLVE) because it is difficult to pursue an agenda that includes formal verification unless the semantics of specifications and implementations are defined together. Perhaps our ideas about the semantics of specifications can suggest new ways for those who work with separate specification and implementation languages to integrate their semantic spaces. An integrated semantic treatment seems essential in order to avoid pitfalls in reasoning about software systems which several authors have exposed [Coo78,EHMO91,Lea91,EHO94,LW94,SWO97].

Our ideas about templates also might encourage the software engineering formal methods community to consider templates more seriously. While RSRG (like [Gog84]) has concluded that templates are inevitably at the very heart of component-based systems [Gib97] and templates have appeared in more and more modern programming languages, most of the formal methods community has hardly mentioned them. We should note that the centrality of templates also seems clear to some, but not all, of the functional representation community in AI.

RESOLVE is unusual in that it is a combination specification-and-implementation language with modern features such as templates, some forms of inheritance, etc. The semantic spaces developed to date for RESOLVE component varieties do not directly follow the approach suggested here. They are based on the ACTI formal model of software subsystems [Edw95], which has heavily influenced this paper. In particular the ACTI semantic space for templates (``concrete templates'', tantamount to $\mathcal{T}$)suggests our proposed view of templates, and the ACTI semantic space for ``abstract templates'' suggests our proposed view of specification templates mentioned at the end of Section 2.4.