We describe a way to develop and implement communications protocols so they are logically sound and meet stated requirements. Our methodology employs a software system called the coordination-specification analyzer (COSPAN) to facilitate logical testing (in contrast to simulation or system execution testing). Logical testing of a communications protocol is carried out on a succession of models of the protocol. Starting with a high-level model (e.g., a formal abstraction of a protocol standard), successively more refined (detailed) models are created. This succession ends with a low-level model which is in fact the code that runs the ultimate implementation of the protocol. Tests of successive models are defined not by test vectors, but by user-defined behavioral requirements appropriate to the given level of abstraction. Testing a high-level design permits early detection and correction of design errors. Successive refinement is carried out in a fashion that guarantees properties proved at one level of abstraction hold in all successive levels of abstraction. We recount the experience of an application of this methodology, employing COSPAN, to develop (analyze and implement in software) a new session protocol at an interface of an AT&T product called the Trunk Operations Provisioning Administration System (TOPAS).
Har'el et al. (Tue,) studied this question.