Formal Specifications and Design of a Message Router
Abstract
Formal derivation refers to a family of design techniques that entail the development of programs which are guaranteed to be correct by construction. This paper investigates the possible application of one such technique-- UNITY-style specification refinement-- to industrial-grade problems. The formal specification and design of a message router illustrates the derivation process and helps identify those methodological elements that are likely to contribute to successful use of this technique in industrial environment. Although, the message router cannot be characterized as being industrial-grade, it is a sophisticated problem that pose significant specification and design challenges-- its apparent simplicity is rather deceiving, The main body of the paper consists of a complete formal specification of the router and a series of successive refinements that eventually lead to a trivial construction of a correct UNITY program. Each refinement is accompanied by its design rational and is explained both formally (proofs being included in an appendix) and informally, in a manner accessible to a broad audience. We use this example to make the case that program derivation provides a good basis for introducing rigor in the design strategy, regardless of the degrees of formality one is willing to consider.