The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.12 - December (1994 vol.20)
pp: 900-913
ABSTRACT
<p>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.</p>
INDEX TERMS
formal verification; open systems; local area networks; transport protocols; online operation; distributed processing; access protocols; observer concept; formal online validation; self-checking distributed systems design; erroneous behavior detection; observable output level; continuous checking; reference; formal verified model; quasi-self-checking observers; industrial LAN; broadcast service; virtual ring MAC protocol testing; link layer; transport layer; OSI layering management; open system architecture; run-time validation; Petri net based models; performance measurements; layered distributed architectures; formal description techniques
CITATION
M. Diaz, J.-P. Courtiat, "Observer-A Concept for Formal On-Line Validation of Distributed Systems", IEEE Transactions on Software Engineering, vol.20, no. 12, pp. 900-913, December 1994, doi:10.1109/32.368136
25 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool