A framework for formal methods driven verification and validation of dependable real-time protocols

Dependable systems such as aircraft control systems, nuclear power plants and medical life-support systems have stringent operational and timing constraints. Failures in these systems result in severe and often unacceptable consequences. Computers used for such critical applications increasingly rely on dependable (fault-tolerant) real-time protocols to deliver reliable and timely services. Developing dependable real-time protocols is a difficult problem. Equally important, and sometimes more difficult, is to “verify” the correctness of the design of the protocol and “validate” the correctness of its implementation in an actual operational environment. The major concern is with helping designers ascertain whether or not the system being designed works correctly. Verification and validation (V&V) is the generic term for methods employed to ensure that the system meets its requirements, and that the requirements meet the needs of the system designer.; The design and testing of dependable real-time protocols involves investigating the large number of state space and possible execution paths in the protocol operation. The conventional V&V techniques use simulation and prototyping over selected sample cases. As systems become more complex, these techniques are not sufficient to assure desired dependability. This research develops a rationale and introduces a novel framework utilizing formal (mathematically rigorous) methods to guide and supplement existing V&V techniques. We have developed structures to graphically represent protocol attributes and information gathered through the formal specification and verification process. The representation structures facilitate the identification of specific test cases for validation.; We have applied our proposed approach to a variety of dependable real-time protocols. Over these studies, we observed that most of these protocols can be designed and implemented using a few functional primitives and their variations. In this context, basic functional building blocks have been identified for their subsequent reuse in formulating (and modularizing) different dependable real-time protocols. We have developed a general approach for protocol composition utilizing these building blocks, as well as guidelines to formally verify the composite protocol. In summary, our proposed formal representation structures and building block approach to protocol composition help generate novel validation strategies for high dependability operations.