Version imprimable |
Vérification d’invariants de systèmes paramétrés par superposition (Superposition based verification of invariants. Application to parameterized systems) | ||
Couchot, Jean-François - (2006-04-06) / Université de Franche-Comté - Vérification d’invariants de systèmes paramétrés par superposition en : Français Directeur(s) de thèse: Bellegarde , Françoise ; Giorgetti, Alain Laboratoire : LIFC Ecole doctorale : SPIM Classification : Informatique | ||
Mots-clés : vérification, invariant, méthode B, superposition, paramètres, Systèmes Uniformes Distribués Résumé : Le prouveur de théorèmes haRVey implante une procédure de décision pour les formules équationnelles non quantifiées dans des théories des tableaux. Ce travail étudie son applicabilité à la vérification, par construction d'invariants, de propriétés de sûreté exprimées sur des systèmes paramétrés. La correction du programme paramétré doit être assurée pour toutes les valeurs des paramètres, interdisant le model-checking. Elle peut s'entreprendre par un calcul de point fixe dont les conditions d'évolution sont déchargées dans un prouveur supportant les formules quantifiées. Graf et Saïdi ont ouvert cette voie en exploitant le prouveur PVS. D'autres ont suivi en exprimant leur système à l'aide de contraintes arithmétiques linéaires obtenues par une abstraction de comptage. Nous proposons un cadre plus basique mais unificateur où les paramètres sont des ensembles finis. Nous montrons que ce cadre convient pour des exemples industriels et des systèmes uniformes distribués. Les spécifications sont écrites dans le langage des machines abstraites B et nous exploitons les calculs de plus faible précondition déjà définis pour cette méthode. Nous introduisons ensuite un calcul de point fixe, obtenu par raffinement d'un calcul de point fixe trivial. Nous proposons ensuite diverses traductions en logique équationnelle des conditions d'évolution, dans l'objectif de faire converger le plus rapidement le prouveur haRVey qui les décharge. Nos expérimentations sur un exemple industriel montrent que la démarche supplante celle du prouveur de l'Atelier B. Théoriquement, nous montrons la décidabilité de certaines obligations de preuve dans le cadre de systèmes uniformes distribués. Résumé (anglais) : The haRVey theorem prover implements a decision procedure for ground first order equational formulae in the array theory. This work provides valuable insights into the applicability of such a prover for the verification of safety properties expressed by an invariant on parameterized systems. The soundness of such parameterized programs has to be checked uniformly, i.e. once for all its sizes. Such programs can be verified by a deductive fix point calculus whose proof obligations are discharged into a prover that allows quantified formulae. Initiated by Graf and Saïdi who discharged their evolution conditions into the PVS prover, many studies have concerned the systems based on linear arithmetic constraints after a convenient counting abstraction. We suggest a more basic but unifying approach in which the parameter ranges over a finite set. We show that such a framework is adequate for industrial test cases and uniform distributed systems. The specifications are written with the set theoretical B machine notation and we exploit an existing weakest precondition calculus for this method. Then, we introduce an invariant strengthening calculus, obtained as the refinement of a trivial calculus. We provide different methods for translating the evolution condition of this calculus into some equational logics. Their main objective is to make haRVey discharge them as fast as possible. On an industrial scale example, we show that this approach is more efficient than the Atelier B deductive system. Theoretically, we prove the evolution condition decidability, where the framework is some uniform distributed systems among broadcast and rendez-vous synchronization. Identifiant : UFC-347 |
Exporter au format XML |