This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Observer-A Concept for Formal On-Line Validation of Distributed Systems
December 1994 (vol. 20 no. 12)
pp. 900-913

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.

[1] J. M. Ayache, P. Azema, and M. Diaz, "Observer, a concept for on line detection for control errors in concurrent systems," in9th Int. Symp. FTC, Madison, June 1979.
[2] J. M. Ayacheet al., "Software redundancy for error detection in distributed systems,"Congrés Fiabilitéet Maintenabilité, Toulouse, Sep. 1982.
[3] G. Lamarche and P. Tallibert, "IDA: Software test language and associated tools," in1st Colloque Génie Logiciel, June 1982.
[4] D. L. Parnas, "The use of precise specifications in the development of software,"Proc. IFIP, 1977, pp. 861, 867.
[5] D. Rayner, "Towards standardised OSI conformance tests,"Protocol Specification, Testing and Validation, V. Diaz, Ed. Amsterdam, Netherlands: North Holland, 1986.
[6] B. Pradinet al., "OGIVE: un outil graphique interactif de vérification des systèmes parallèles décrits par des réseaux de Petri,"Revue MICADOSep. 1980.
[7] H. Zimmermann, "OSI reference model--The ISO model of architecture for Open Systems Interconnection,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 425-432, Apr. 1980.
[8] M. A. Fischler, O. Firchtein, and D. L. Drew, "Distinct software: an approach to reliable computing," in2nd USA-Japan Comp. Conf., pp. 27-4-1, 27-4-7.
[9] B. Randell, "System structure for software fault tolerance,"IEEE Trans. Software Eng., I:2, pp. 220-232, June 1975.
[10] J. R. Kane and S. S. Yau, "Concurrent software fault detection,"IEEE Trans. Software Eng., I:1, pp. 87-99, Mar. 1975.
[11] M. Diaz, "Specification and validation of communication and co-operation protocols using Petri net based models,"Computer Networks, Dec. 1982.
[12] G. V. Bochmann and C. A. Sunshine, "Formal methods in communication protocol design,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 624-631, Apr. 1980.
[13] A. Danthine, "Protocol representation with finite-state models,"IEEE Trans. Commun., vol. COM-28, no. 4, Apr. 1980.
[14] H. J. Genrich and K. Lautenbach, "The analysis of distributed systems by means of predicate/transition nets," inSemantics of Concurrent Computation, G. Kahn Ed. New York: Springer-Verlag, 1979, pp. 123-146; also in Lect. Notes in Computer Sciences, vol. 70.
[15] G. Bochmann, "A general transition model for protocols and communication services,"IEEE Trans. Commun., vol. 28, pp. 643-650, 1980.
[16] Manuel de présentation de FACTOR, APTOR (1984).
[17] J. M. Ayache, J. P. Courtiat, and M. Diaz, "Self-checking software in distributed systems,"3rd Int. Conf. Distrib. Comput. Syst. IEEE, Oct. 1983.
[18] J. M. Ayache, J. P. Courtiat, and M. Diaz, "REBUS, a fault-tolerant distributed system for industrial real-time control,"IEEE Trans. Comput., Special Issue on Fault Tolerant Computing, vol. 31, no. 7, Jul. 1982.
[19] P. Azemaet al., "Specification and verification of distributed systems using Prolog interpreted Petri nets," inProc. IEEE 7th Int. Conf. Software Eng., 1984, pp. 510-518.
[20] ISO, "Estelle, a formal description technique based on an extended state transition model,"ISO-TC97-SC21-WG1, DIS 9074.
[21] ISO, "LOTOS, a formal description technique based on an extended state transition model,"ISO-TC97-SC21-WG1, DIS 8807.
[22] G. Juanole and B. Algayres, "Protocol design and modeling," in4th European Workshop on Application and Theory of Petri Nets, Toulouse, Sept. 1983.
[23] M. Diaz, "Petri net based models in the specification and verification of protocols," LNCS, no. 255,Advances in Petri Nets, E. Braueret al., Eds. New York: Springer-Verlag, 1987.
[24] R. Molva, "Conception et réalisation d'un observateur d'architectures multicouches," Thèse de Doctorat, Univ. Paul Sabatier, Toulouse, Oct. 1986.
[25] J. M. Novali, "Modèles d'observation pour les architectures multicouches," Thèse de Docteur-Ingénieur, Toulouse, INSA, Nov. 1986.
[26] D. A. Anderson and G. Metze, "Design of totally self-checking circuits form-out-of-ncodes,"IEEE Trans. Comput., vol. 22, Mar. 1973.
[27] M. Diaz, P. Azema, and J. M. Ayache, "Unified design of self-checking and fail safe combinational circuits and sequential machines,"IEEE Trans. Comput., vol. 28, no. 3, pp. 276-281, Mar. 1979.
[28] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE-13, no. 3, pp. 386-397, Mar. 1987.
[29] F. Biairdi, N. D. Francesco, and G. Vaglini, "Development of a debugger for a concurrent language,"IEEE Trans. Software Eng., vol. SE-12, pp. 547-553, Apr. 1986.
[30] M. Diaz and C. Vissers, "SEDOS, Estelle and LOTOS environments for the design of open distributed systems,"IEEE Software Eng., vol. 15, Nov. 1989.
[31] J. C. Lloret and P. Azema, "Incremental verification of token ring protocol," in6th Int. Workshop on Protocol Specification, Testing and Validation, Montreal, June 1986.
[32] R. J. van Glabbeek, "The linear-branching time spectrum," inProc. CONCUR89, LNCS 458, J. Baeten&J. Klop Eds. New York: Springer-Verlag, 1990, pp. 278-287.
[33] Z. Kohavi, "Switching and finite automata theory,"Computer Science series. New York: McGraw-Hill, 1970.
[34] M. Hennessy and R. Milner, "Algebraic laws for nondeterminism and concurrency,"J. ACM, vol. 32, no. 1, pp. 137-161, Jan. 1985.
[35] R. Milner,Communication and Concurrency. Englewood Cliffs, NJ: Prentice-Hall International, 1989.

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, G. Juanole, 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, Dec. 1994, doi:10.1109/32.368136
Usage of this product signifies your acceptance of the Terms of Use.