Reactive system verification case study: Fault-tolerant transputer communication

Summary and computer operating systems. Reactivesystems areoften naturally modeled (for logical design purposes) as aA reactive program is one which engages in an ongoing composition of autonomous processes which progressinteraction with its environment. A system which is concurrently andwhich communicate to share informa-° controlled by an embedded reactive program is called a tion and/or to coordinate activities. Reactive systems arereactive system. Examples of reactive systems areaircraft nondeterministicin that the sequence of events is notflight management systems, bank automatic teller specified but depends on actionsof the environment.' machine (ATM) networks, airline reservation systems Reactive system specifications often include responseand computer operating systems. Reactive systems are time requirements.often naturally modeled (for logical design purposes) as acomposition of autonomous processes whichprogress Thesereactive system process characteristics (autono-concurrently and which communicate to share mous, concurrent,communicating, nondeterministic, andinformation and/or to coordinate activities, time sensitive) have forced thedevelopment of newapproaches to verify that a reactive system satisfies itsFormal (i.e., mathematical) frameworks for system specification. As noted by Alur (ref. 3), "The number ofverification are tools used to increase theusers' confi- formalisms that purportedly facilitate the modeling,dence that a system design satisfies its specification. A specifying andproving of timing properties for reactiveframework for reactive system verification includes systemshas exploded over thepast few years." Theformal languages for system modeling andfor behavior diversity of process communication and coordinationspecification and decision procedures and/or proof- constructs and thevariety of specifications of interestsystems for verifying that the system model satisfiesthe have contributed to this profusion of frameworks. Thesystem specifications, features required to further improve next-generationIn the study reported here, using the Ostroff framework frameworks can best be determined through use andfor reactive system verification, an approach to achieving evaluation of currently available frameworks in manyfault-tolerantcommunication between transputers was diverse applications. One objective for this report is toshown to be effective. The keycomponents of the design, contributeto that evolutionary process.the decoupler processes, maybe viewed as discrete-event- The framework chosen for the analysis of aparticularcontrollers introduced to constrain system behavior such system mustallow faithful modeling of essential systemthat system specifications are satisfied, features in order to reliably infer system behavior fromThe Ostroff framework was also effective.The expres- model behavior. In the study reported here, a frameworksiveness of the modeling language permitted construction developed by Ostroff was applied to verify an approach toof a faithful model of the transputer network.The relevant achievefault-toleranttransputer communication. Inthespecifications were readily expressed in the specification following sections, we outline the Ostroff framework,language. The set of decision procedures provided was reviewthe approach to fault-toleranttransputer communi-adequate to verify the specifications of interest, cation verified, describe the Transputer Network Model,and discuss verification procedures and verificationThe need for improved support for system behavior results. The need for improved support for systemvisualization is emphasized, behavior visualization is emphasized.