Multiparadigm Specification

Many formal languages and notational styles have been proposed for specification. There is reason for this diversity. Each paradigm offers a different set of expressive capabilities, appropriate for specifying clearly and concisely a different set of properties. Each paradigm also offers a different set of analytic capabilities, appropriate for rigorous reasoning about a different set of properties.

In my experience, no large software system is homogeneous enough to fit a single specification paradigm. Thus practical specification of large software systems requires composition of specifications written in different paradigms.

Early forays into this subject include:

The last paper won the Best Paper of 1989 Award from IEEE Software in 1990.

More recently, I worked on this subject with Michael Jackson. Our basic results can be found in "Conjunction as composition" (Pamela Zave and Michael Jackson; ACM Transactions on Software Engineering and Methodology II(4):379-411, October 1993).

In this paper, a multiparadigm specification is the composition of a finite set of partial specifications. For the purposes of understanding the meaning of this composition, and of assigning a semantics to it, a partial specification is equivalent to an assertion in one-sorted first-order predicate logic with equality. The composition of a set of partial specifications is equivalent to the conjunction of their equivalent assertions.

To elaborate the above point, each specification language used has an algorithm for translating specifications in the language to assertions in first-order logic. These translations are used to answer questions such as: Are these partial specifications consistent? How do they constrain one another? Conjoined, do they say everything that needs to be said? The translation may omit some of the meaning of the original, but only if the omitted aspects of the language's meaning do not affect the answers to the first two of these questions.

"Conjunction as composition" is very general, and gives little guidance on constructing actual multiparadigm specifications. We followed up that work by developing a specific multiparadigm technique in which Z is supplemented, primarily with automata and grammars, to provide a rigorous and systematic mapping from input stimuli to convenient operations and arguments for the Z specification. The technique is explained in "Where do operations come from? A multiparadigm specification technique" (Pamela Zave and Michael Jackson; IEEE Transactions on Software Engineering XXII(7):508-528, July 1996), which delimits the applicability of the technique, applies it to two examples, and shows how to analyze the resulting specifications for consistency.

Peter Mataga and I used this technique to write a formal specification of a switching system that controls modern, time-multiplexing telephones and offers twelve other features. This system appears to be an order of magnitude more complex than the targets of other published switching specifications. An overview of this specification can be found in "Multiparadigm specification of an AT&T switching system" (Peter Mataga and Pamela Zave, Applications of Formal Methods, Michael G. Hinchey and Jonathan P. Bowen, editors, Prentice-Hall International, 1995). The full specification can be found in the following three technical memoranda, jointly titled "A formal specification of some 5ESS(R) features": Overview (Part I), Telephone states and digit analysis (Part II), Connections and provisioning (Part III).

The paper "Formal description of telecommunication services in Promela and Z" (Pamela Zave, Calculational System Design (Proceedings of the 19th International NATO Summer School), Manfred Broy and Ralf Steinbruggen, editors, IOS Press, 1999) presents yet another multiparadigm specification, combining Z and Promela in yet another way.