Exhaustive analysis and simulation for distributed systems, both sides of the same coin
Tóm tắt
This paper presents exhaustive analysis and simulation for distributed systems validation. Exhaustive analysis makes possible to detect quickly several types of errors, for instance, unspecified reception of signals, errors in timer management, deadlock, errors in precedence, etc. But, in general, exhaustive analysis can only be applied to a simplified model of the distributed system due to the state explosion problem. On the other hand, simulation permits accurate tests and confronts the distributed system to complex situations. We think both forms of validation are complementary. Validation was done on systems specified in the SDL language, using OVAL, a tool for specification validation developed at CNET, Paris A. This tool allows exhaustive analysis and simulation of SDL specified systems. We illustrate our results with several examples.
Tài liệu tham khảo
Paul È (1987) Manuel OVAL version October 1987, Note Technique NT/PAA/CLC/LSC/2092 (October 1987) CNET Paris A
Cavalli AR, Horn F (1987) Proof of specifications by using finite state machines and temporal logic. IFIP 7th Symposium on Protocol specification, testing, and verification VII, Zurich (May 1987) North Holland
Maigron P (1987) Une interface LDS/réseaux de Petri, Note Technique NT/PAA/CLC/LSC/1938 (March 1987) CNET Paris A
Cavalli AR, Paul E (1987) Deux exemples d'utilisation de l'outil OVAL pour la validation de spécifications LDS. Note Technique NT/PAA/CLC/LSC/2049 (September 1987) CNET Paris A
Raynal M (1985) Algorithmes distribués et protocoles. Eyrolles, Paris 1985
Chang E, Roberts R (1979) An improved algorithm for decentralized extrema finding in circular configurations of processors. Commun ACM, 22: 281–283
Bourguet-Rouger A, Camacho J, Martin M (1988) Edition structurelle graphique: application au langage de spécification LDS du CITT, Poster “Software Engineering”, AFCET, Paris (October 1988)
Jard C, Monin JF, Groz R (1985) Veda: un outil pour la validation et l'evaluation d'algorithmes distribués. Présentation génerale et manuel d'utilisation. Note Technique CNET NT/LAA/SLC/203 (April 1985)
Groz R (1986) Unrestricted verification of protocol properties on a simulation using an observer approach. In: Bochmann G, Sarikaya B (eds) VI IFIP WG6. 1 Workshop Gray Rocks, Montreal, Canada (June 1986) North Holland
Pradin B (1979) Un outil graphique interactif pour la vérification des systèmes à évolutions paralléles décrits par réseaux de Petri, Thèse de Docteur-Ingénieur, Université Paul Sabatier, Toulouse, 1979
Fernandez JC, Richier JL, Voiron J (1985) Verification of protocol specifications using the cesar system. Proc 5th Int Workshop on protocol specification, testing and verification. North Holland, France
CONCERTO, Atelier de Logiciel, Presentation Technique, CNET Lannion A (February 1986) Perros-Guirec, France