Formal Specifications for Packet Communication Systems.
Abstract
One of the most difficult tasks facing computer scientists is that of designing systems and making sure that they perform their intended functions correctly. As computer systems have grown in size and complexity, the problems of system design and verification have become increasingly acute. Formal specifications, which are precise descriptions of a system's function, provide a basis for understanding system operation as well as for proving correctness. Although there has been much work in formal specification and verification of computer programs, relatively little research has been done on system specification. A particular class of asynchronous systems, known as packet communication systems, has been chosen as the subject of this study. Packet communication systems are composed of independently operating units that interact only by transmitting packets of information. These systems possess a number of desirable structuring properties that make them suitable for formal analysis. We have developed a model for formally describing the behavior of packet systems and for proving correctness. The model is based on the fact that packet systems may be viewed both externally, in terms of their interaction with the outside world, and internally, in terms of their structural composition from smaller units.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1977
- Accession Number
- ADA048980
Entities
People
- David J. Ellis
Organizations
- Massachusetts Institute of Technology