Techniques d'abstraction dans la verification des systèmes concurrents

Comme les systemes mat eriels et logiciels grandissent de fa con continue en echelle et fonctionnalit es, la probabilit e d erreurs subtiles de- vient toujours plus grande. Les techniques d abstraction, souvent bas ees sur l interpr etation abstraite de Cousot, fournissent une m ethode pour ex ecuter symboliquement les systemes en utilisant le domaine abstrait a la place du domaine concret. Dans cette these, on introduit des techniques d abstraction pour les logiques sous des interpr etations multi-valu ees. Beaucoup d applications des logiques multi-valu ees ont et e trouv ees dans la v erification du mat eriel et du logiciel. Pour la v erification du mat eriel, des outils de simulation et des r ealisations des circuits multi-valu es v eritables ont et e propos es, les risques dynamiques ont et e model es en introduisant des etats faux pour trouver des r egions chevauchantes des signaux en concurrence, etc. Pour la v erification du logiciel on a besoin d incertitude parce qu on ne peut savoir si certains comportements devraient etre possibles et on a besoin du d esaccord parce que l on peut avoir des acteurs diff erents qui sont en d esaccord pour la maniere dont les systemes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d equivalence et apres, les symboles pr edicatifs de la logique sont red efinis a s appliquer cor- rectement aux classes d equivalence a l aide des politiques d interpr etation. On fournit des r esultats de pr eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu ees pour la logique temporelle, nous pr esentons une etude de cas pour utiliser l abstraction dans le contexte des modeles du contr ole d acces. Nous fournirons aussi une technique d abstraction pour les types de do- nn ees. Cette technique d abstraction peut etre elargie pour les types abstraits de donn ees. Ici, les abstractions sont appliqu ees aux sp ecifications initiales au moyen des equations et ils sont appel es des abstractions equationnelles. De plus, la technique d abstraction pr esent ee g en eralise et clarifie la nature de beaucoup de techniques d abstraction trouv ees dans la litt erature, telles: la technique de dupliquer les symboles pr edicatifs, shape analysis, l abstraction par pr edicats, l approche de McMillan, etc. Pour raisonner au sujet des systemes dynamiques, on introduit les types de donn ees dynamiques et on etend la m ethode d abstraction ant erieure a ce cas. Le probleme principal qui survient quand on utilise les abstractions est de trouver l abstraction convenable ou de raffiner une abstraction d eja existante pour en obtenir une meilleure. On prouve que les techniques d abstraction que nous avons introduites pour les types de donn ees sous l interpr etation 3- valu ee Kleene, peuvent etre utilis ees dans une proc edure de raffinement. De plus, on montre que la proc edure de raffinement guid e par contre-exemple est plus efficace quand on l utilise sous les abstractions equationnellesAs the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractionsPARIS-EST-Université (770839901) / SudocSudocFranceF