Formal Verification in the Polyhedral Model ; Vérification Formelle dans le Modèle Polyédrique

This document deals with formal verification of safety properties in the context of embedded systems design. This work is based on the polyhedral model formalism, the combination of systems of affine recurrence equations with integer polyhedra. This model is used in high level synthesis fot generating parallel architectures from regular system descriptions, dimensions of which are defined by means of symbolic parameters. We are interested in the verification of safety properties about boolean control signals that are generated or manually introduced during the synthesis. We call control properties properties on such signals. We show in this document that the polyhedral model is well suited to the formal verification of control properties. In this work, we present a ``polyhedral logic'' that allows for specifying and proving properties in the polyhedral model. The syntax and semantics of logical formulae are based on those of a description language designed for systems of affine recurrence equations on polyhedral domains. There are different kinds of deductions rules: ``classical rules'' on logical connectors, rewriting rules and rules induced by the computations in the model. We present an algorithm to automatize the proof construction, and heuristic techniques to speed up this construction. These algorithms allow for proving simple properties like the fact that a signal is always true for a given set of processors and time instants. We then sketch and begin to develop solutions that can be used to expand our logic so as to express and prove more complex properties, like mutual exclusion properties for instance. We give some proof tactics for this augmented formalism. ; Les travaux présentés dans ce document sont orientés vers la vérification formelle de propriétés de sûreté dans le cadre de la conception des systèmes enfouis. Nous nous plaçons dans le formalisme du modèle polyédrique, combinaison des systèmes d'équations récurrentes affines avec les polyèdes entiers. Ce modèle permet de faire de la synthèse de ...