Formal protocol design using partial constraints

Formal design of communication protocols using partial constraints is presented. Partial constraints are modal logic formulae constructed from requirements, using three basic connectives: the nondeterministic "or" the "precedence" and the "followed by" operator. Every formula is satisfied by a class of related behaviors. Partial specifications satisfy those partial constraints from which they are generated; thus, correctness concerns are reliably treated. The method leads to extensional specifications. The method is illustrated with a portion of the Express Transfer Protocol (XTP) specification