Title :
Observer-a concept for formal on-line validation of distributed systems
Author :
Diaz, Michel ; Juanole, Guy ; Courtiat, Jean-Pierre
Author_Institution :
Lab. d´´Analyse et d´´Archit. des Systemes, CNRS, Toulouse, France
fDate :
12/1/1994 12:00:00 AM
Abstract :
Proposes the observer concept for designing self-checking distributed systems, i.e. systems that detect erroneous behaviors as soon as errors act at some observable output level. The approach provides a solution to build systems whose on-line behavior is checked against a formal model derived from a formal description. In other words, the actual implementation is continuously checked against a reference, this reference being a formal and verified model of some adequately selected aspects of the system behavior. The corresponding methodology, the software concepts and some applications of the observer are presented. General definitions are given first that theoretically define self-checking systems as systems that include and implement complete on-line validation. The basic concepts and the difficulties to implement self-checking validation are then given. In order to provide simple implementations, the previous definitions are weakened to design quasi-self-checking observers for LANs using a broadcast service. Three specific applications are given to illustrate the proposed approach: testing a virtual ring MAC protocol, checking the link and transport layers in an industrial LAN, and managing a complete OSI layering, from layer 2 to layer 6, in an open system architecture
Keywords :
access protocols; distributed processing; formal verification; local area networks; online operation; open systems; transport protocols; OSI layering management; Petri net based models; broadcast service; continuous checking; erroneous behavior detection; formal description techniques; formal online validation; formal verified model; industrial LAN; layered distributed architectures; link layer; observable output level; observer concept; open system architecture; performance measurements; quasi-self-checking observers; reference; run-time validation; self-checking distributed systems design; transport layer; virtual ring MAC protocol testing; Application software; Broadcasting; Local area networks; Measurement; Media Access Protocol; Open systems; Petri nets; Runtime; System testing; Transport protocols;
Journal_Title :
Software Engineering, IEEE Transactions on