Our research concerns the construction of complex distributed software applications that have to satisfy strong requirements concerning functional correctness and reliability. An industrial solution to tackle this complexity is the definition of a suitable underlying architecture which provides high-level communication mechanisms and construction rules for the components. This architecture should be general enough to be suitable for a whole family of products. Our aim is to combine this solution with another technique to increase the quality and reliability of applications, namely the use of formal methods. This means that there are precise mathematical models for specifications and implementations and suitable techniques to relate the two.
As a specific case study we consider the software architecture Splice, as devised by the company Hollandse Signaalapparaten. It forms the core of many of their products, especially in the field of command and control systems. Typically, such systems receive large streams of data from sensors which are used to build a coherent image of the environment and to take appropriate action on the basis of this information. Additionally, the internal representation is visualized for operators which interact with the system. All these tasks are carried out by a large number of parallel processes. Splice can be seen as a coordination language that provides a suitable communication mechanism where processes need not know the producers of the data they need or the consumers of the data they produce. Important is that Splice allows dynamic reconfiguration of the system and, for instance, duplication of processes, thus achieving a high degree of reliability and fault-tolerance.
Other work [9,10] has addressed the formalization of the requirements of such command and control systems. This has resulted in a structured specification in the language of the interactive theorem prover PVS . Our aim is to define a verification method to prove that a Splice program satisfies such a specification. To be able to deal with large programs, we aim at a compositional framework which allows reasoning by means of the interface specifications of components, without knowing their implementation .
As a starting point for such a verification method, a formal definition of the Splice interaction primitives is needed. There is already some work on the semantics of Splice, e.g. a comparison of semantic choices using an operational semantics [3,4] and a process algebra framework . We aim at a denotational semantics, however, since this is the proper starting point for compositional reasoning. Furthermore, we would like to investigate which choice of Splice primitives is most convenient for high-level reasoning and, at the same time, allows efficient implementation. Finally, to achieve convenient tool support for our work and a clear relation with the requirements specification, our semantics will be formulated in the language of PVS.