Abstract FR:

Les systemes vises sont temps-reel multitaches complexes importants pour la surete. Pour valider le comportement de tels systemes, il est necessaire d'abstraire un modele rigoureux et equivalent. Les travaux menes dans le cadre de leur la validation portent sur le type d'abstraction utile et exploitable de ces systemes. Notre approche de la verification se fonde sur les reseaux de petri ordinaires (rdp) ou equivalents. L'integration du temps conserve leur theorie mathematique. L'ecoulement du temps est caracterise par le tirage de certaines transitions du reseau, qui sont identifiables dans le graphe de marquage et qui peuvent etre utilisees pour l'etude des proprietes recherchees. Les invariants sont en rapport avec le temps et representent un moyen efficace pour verifier la consistance du modele. Les proprietes sont verifiees sur le reseau (modele) construit a partir de l'application. Le principe repose sur la notion de motifs reutilisables. Les rdp fournissent un graphe de marquage au formalisme simple. Ce graphe est reduit par des methodes de bisimulation. On procede a une analyse du resultat obtenu par model-checking et proof-checking. Le model-checking est realise sur des graphes reduits ou issus de la decomposition en modules (possedant des proprietes) du rdp. Nous avons defini l'operateur de reduction avec le choix de la congruence (adaptee aux proprietes recherchees par model-checking) retenue et mise en uvre. Nous avons aussi defini l'operateur de produit synchronise avec les caracteristiques des graphes reduits. Il est mis en evidence la conservation des proprietes dans le graphe issu du produit synchronise de sous-graphes de marquage (issus de parties rendues autonomes du rdp global) eux-memes reduits. La recherche de proprietes peut se faire a partir de l'analyse des graphes de marquage engendres par des parties du rdp global. Cette decomposition modulaire de la preuve et de la validation permet d'aborder des problemes de taille plus importante.