Architecture-Driven Verification of Concurrent Systems

This paper proposes a method to construct a set of proof obligations from the architectural specification of a concurrent system. The architectural specifications used express correctness requirements of a concurrent system at a high level without any reference to component functionality. Then the proof obligations derived from such specifications are discharged as model checking tasks in a suitable behavioral model where components are assigned their respective functionalities. An experimental extension to the SPIN tool is used as the model checker. The block diagram notation used to specify architectures allows interchangeable components with equivalent intended functionalities to be encapsulated within a representative module. A proof obligation of such a system is discharged as an equivalence checking task in the behavioral model chosen. It is shown how infeasible proof obligations can be decomposed by decomposing the architectural specification. Obligation decomposition relies on assume-guarantee conditions.Cet article propose une m\ue9thode de construction d'un ensemble d'obligations de preuve \ue0 partir de la sp\ue9cification architecturale d'un syst\ue8me concurrent. Cette sp\ue9cification architecturale exprime les exigences d'exactitude d'un syst\ue8me concurrent \ue0 un niveau \ue9lev\ue9, sans faire r\ue9f\ue9rence aux fonctionnalit\ue9s des composants. Les obligations de preuve d\ue9riv\ue9es de cette sp\ue9cification sont exprim\ue9es sous la forme de t\ue2ches de v\ue9rification du mod\ue8le, dans un mod\ue8le de comportement pertinent, dans lequel les composants se voient attribuer leurs fonctionnalit\ue9s respectives. Une extension exp\ue9rimentale de l'outil SPIN est utilis\ue9e comme v\ue9rificateur ou contr\uf4leur de mod\ue8le. La notation des sch\ue9mas synoptiques utilis\ue9e pour sp\ue9cifier l'architecture permet d'encapsuler dans un module repr\ue9sentatif des composants interchangeables ayant des fonctionnalit\ue9s cibles \ue9quivalentes. Une obligation de preuve d'un tel syst\ue8me est repr\ue9sent\ue9e sous la forme d'une t\ue2che de v\ue9rification de l'\ue9quivalence dans le mod\ue8le de comportement choisi. On d\ue9montre comment des obligations de preuve irr\ue9alisables peuvent \ueatre d\ue9compos\ue9es, en d\ue9composant la sp\ue9cification de l'architecture. La d\ue9composition des obligations est fond\ue9e sur des conditions d'hypoth\ue8se garantie.NRC publication: Ye