During the last several years, we have explored temporal logic as a framework for specifying and reasoning about concurrent programs, distributed systems, and communications protocols. Previous papers[Schwartz/Melliar-Smith81, 82, Vogt82a,b] report on our efforts using temporal reasoning primitives to express very high-level abstract requirements that a program or system is to satisfy. Based on our experiences with those primitives, we have developed an interval logic more suitable for expressing higher-level temporal properties.

This paper describes the formal specification and proof methodology employed to demonstrate that the SIFT computer meets its requirements. The hierarchy of design specifications is shown, from very abstract descriptions of system function down to the implementation. The most abstract design specifications are simple and easy to understand, almost all details of the realization having been abstracted out, and can be used to ensure that the system functions reliably and as intended. A succession of lower level specifications refine these specifications into more detailed and more complex views of the system design, culminating in the Pascal implementation. The paper describes the rigorous mechanical proof that the abstract specifications are satisfied by the actual implementation.

This paper attempts to lend perspective to several different methods that have been employed for specifying computer communication protocols by comparing a spectrum of specification techniques. The paper characterizes specification languages such as state transition diagrams, variants of temporal logic approaches, and sequence expressions by the extent to Which information is encoded as properties of a single state versus properties of a history of the entire computation state sequence. Taking the prototypical alternating bit protocol as an example, each method is used to specify the requirements for the send process of the distributed system.