A methodology for the design and implementation of communication protocols for embedded wireless systems

摘要

Communication protocol design involves 4 complementary domains: specification, verification, performance estimation, and implementation. Typically, these technologies are treated as separate, unrelated phases of the design: formal specification, formal verification, and implementation, in particular, are rarely approached from an integrated systems perspective. For systems that are implemented using a combination of hardware and software, a significant technical barrier to this integration is the lack of an automated, formal mapping from an abstract, high-level specification to a detailed implementation in either synchronous hardware or non-deterministically interleaved software threads.;This dissertation presents a design methodology that uses a combination of formal and informal mappings to refine a high-level specification into an implementation. A taxonomy of formal languages that are commonly used for protocol or finite-state machine (FSM) description is developed and used to identify when a particular formal model is most useful in the design flow. The methodology relies on an informal specification to develop a formal description that can be formally verified at the asynchronous message-passing behavioral level. Central to the methodology is application of compositional refinement verification to relate a synchronous implementation finite-state machine to an asynchronous specification state machine. An architectural template for an embedded communication system is used to facilitate the mapping between the specification and a software implementation, and a prototype operating system and low-level interface units provide the necessary interprocess communication infrastructure between hardware and software.