La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course qui peuvent se produire dans des entrelacements particuliers d'actions de processus et sont par conséquent difficiles à reproduire. Il est souvent non-trivial d'énoncer précisément les propriétés attendues d'un algorithme et les hypothèses que l'environnement est supposé de satisfaire pour que l'algorithme se comporte correctement. La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Des instances finies d'algorithmes écrits en PlusCal-2 peuvent être vérifiées à l'aide du model checker tlc. La deuxième contribution de cette thèse porte sur l'étude de méthodes de réduction par ordre partiel à l'aide de relations de dépendance conditionnelle et constante. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker tlc. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique (comme alternative à l'algorithme dynamique), s'appuyant sur une relation de dépendance constante, et son implantation au sein de tlc. Nous présentons nos résultats expérimentaux et une preuve de correction.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course et sont par conséquent difficiles à reproduire La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker TLC. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique s'appuyant sur une relation de dépendance constante, et son implantation au sein de TLC. Nous présentons nos résultats expérimentaux et une preuve de correction / Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness

En dépit de ses diverses caractérisations, la nature innovante des instruments de politique publique semble consacrer trois types d’innovation : (a) soit, des imitations, à un glissement de modalités près, d’instruments préexistants ; (b) soit des hybridations d’instruments plus ou moins contraignants ; (c) soit des assemblages d’instruments de nature méta-instrumentale. En admettant alors que tous les instruments découlent les uns des autres par le biais de ces trois chemins de conception, nous avons cherché à produire une méthode de conception fondant concomitamment, et autour d’un même modèle-objet, une capacité d’identification ex post des instruments innovants et une capacité ex ante d’innovation.Au terme d’une démarche de recherche-intervention, nous avons convenu de définir les instruments comme autant de chaînes de causalité préfigurées de l’action collective, et avons formulé un langage algorithmique autour d’un certain nombre d’éléments - des acteurs, des actions, des événements, des opérateurs logiques et des vecteurs d’impact – afin de les caractériser de façon ostensive. En consacrant une méthode d’évaluation de la nouveauté et de l’effectivité instrumentales, nous avons dès lors pu établir qu’un instrument est innovant s’il constitue une nouvelle chaîne de causalité opérant effectivement dans la réalité technico-sociale. De façon corollaire, innover un instrument revient alors à dessiner une nouvelle chaîne de causalité, ou à modifier les acteurs et les actions qui la composent.Afin d’illustrer et d’éprouver cette méthode de conception que nous qualifions de combinatoire, nous avons enfin cherché à interroger le caractère innovant du dispositif des certificats d’économie (CEE) et ce, en proposant un protocole d'évaluation et en formulant diverses pistes d'innovation. / Although it is diversely characterized, the innovative nature of instruments seems to follow three types of innovation: (a) imitations of existing instruments; (b) hybridizations of more or less coercive instruments; (c) or meta-conglomerations of instruments. After admitting that all instruments originate from one another through these three innovation paths and a unique object model, we tried to provide a new design method that would both enable the identification of innovative instruments and their design.Within the frame of intervention research, we agreed to define an instrument as a specific intended causal chain of public action, and formulated an algorithmic language along some instrumental elements (actors, actions, events, logical operators and impact vectors) in order to characterize instruments in an ostensive way. After developing a method to evaluate the newness and the effectivity of any instrument, we could more precisely define an innovative instrument as a new causal chain that is effectively implemented in the technical and social reality. As a corollary, innovating an instrument consists in designing a new causal chain, or modifying the actors and actions in it.Eventually, and in order to apply and test what we called a combinatory design method, we chose to question the innovative nature of the Energy Savings Certificates scheme (ESC). For this purpose, we elaborated an evaluation protocol and formulated several possible lines of innovation.

.

.

.