Partially defined specifications

Partially defined specifications are specifications where some parts are left out. Those points in the specification which contain undefined parts, are explicitly marked. The following descriptions of the sender in the alternating bit protocol represent both totally and partially defined versions of the specification.

The main application of partially defined states seems to be a stepwise refinement of protocols. Let S be a service. Develop a chain of specifications

P1, P2, P3, ..., Pn

such that for every i, Pi is in some preorder relation with S. This preorder is such that in the case of totally defined systems it coincides with the corresponding equivalence. If now Pn is totally defined and Pn is in preorder relation with S, then P is in fact equivalent with S. If the preorder relation is not valid for some i, then we have made a design mistake and the partially defined specification cannot be completed in a correct way. Thus design mistakes can be detected at an early stage.

Partially defined specifications were first studied in the article [1]. The above approach was presented in the work [2]. More applications and theory can be seen in [3].

Refrences:

[1] K. Larsen and B. Thomsen: Compositional Proofs by Partial Specification of Processes. Lecure Notes in Computer Science 324, 1988.

[2] U. Celikkan and R. Cleaveland: Generating diagnostic information for behavioural preorders. Distributed Computing 9, pp. 61-75, 1995.

[3] T. Karvi: Partially Defined Lotos Specifications and their Refinement Relations. Ph.D. thesis, University of Helsinki, Department of Computer Science, Series of Publications A, Report A-2000-5.