• DocumentCode
    1246867
  • 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
  • Volume
    20
  • Issue
    12
  • fYear
    1994
  • fDate
    12/1/1994 12:00:00 AM
  • Firstpage
    900
  • Lastpage
    913
  • 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;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/32.368136
  • Filename
    368136