Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Cette thèse s'inscrit dans le cadre des travaux consacrés au développement des modèles sémantiques destinés aux langages de programmation concurrents. Une particularité de notre étude réside dans la considération explicite d'une récursivité au niveau des programmes parallèles. Pour ces programmes nous proposons une sémantique originale, dont nous étudions en détail les propriétés. Bien que le modèle proposé ne soit pas d'états finis, il est possible de le munir d'une structure de systèmes de transitions bien structurés au sens de Finkel ce qui établit la décidabilité de nombreux problèmes de vérification. Cette sémantique à la Plotkin permet de mieux comprendre le comportement des programmes récursifs-parallèles, d'analyser formellement certaines de leurs propriétés, de décrire la stratégie d'implémentation et d'énoncer en quel sens elle est correcte.

Les réseaux de Petri et leurs extensions constituent un formalisme très connu pour la modélisation de la spécification des systèmes à évènements discrets temps réel. Pour ces systèmes, les exigences de vérification et de validation sont indispensables pour garantir leur bon fonctionnement car la moindre erreur peut entrainer des conséquences catastrophiques. Pour analyser le comportement du système, il est courant de construire le graphe d’états (ou espace d’états) qui énumère de façon exhaustive les différents états accessibles.Ce graphe permet de vérifier des propriétés génériques comme le caractère borné, l’accessibilité, la terminaison, la vivacité, l’absence de blocage, etc. Mais la construction de cet espace d’états est confrontée au problème d’explosion combinatoire du nombre d’états lié à la complexité et à la concurrence du système.L’une des alternatives pour contenir cette combinatoire est de conserver uniquement les ordres partiels entre les évènements. Le dépliage est une technique d’ordre partiel adaptée à la vérification, au diagnostic et à la planification. Cette thèse contribue à l’étude du dépliage des réseaux de Petri et, plus particulièrement,apporte une contribution au dépliage des réseaux de Petri avec des arcs de reset. De plus, le dépliage explicite les exécutions possibles du système qui sont, par définition, des processus. Il s’agit plus précisément des processus de branchement qui diffèrent des processus classiques. Ainsi, nous proposons une algèbre adaptée aux processus de branchement issus du dépliage des réseaux de Petri. / Petri nets and their extensions are a well-known formalism for modeling the specification of discrete events systems real-time. For these systems, the demands of verification and validation are essential to ensure their smooth functioning because the least error can lead to catastrophic consequences. To analyze the behavior of the system, it is common to construct the stategraph (or state space) which lists exhaustively the different accessible states. This graph allows to check the generic properties such as boundedness, accessibility, termination, vivacity, the absence of blocking, etc. But building this state space is confronted with the problem of combinatorial explosion of the number of states related to the complexity and concurrence of the system. One of the alternatives to contain this combination is to keep only partial orders between events. Unfolding is a partial order adapted to technical verification, diagnosis and planning. This thesis contributes to the study of the unfolding of Petri nets and, in particular, his contributes to the unfolding of Petri nets with reset arcs. Moreover, the unfolding explains the possible executions of the system which are, by definition, the processes. This is specifically the branching processes that differ from conventional processes. Thus, we propose an algebra adapted to the branching process from unfolding of Petri nets.

EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cette thèse, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking. Dans un premier temps, on présente une sémantique opérationnelle deEB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées. Cette sémantique nous permet de définir une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 une tous les outils de vérification fonctionnelle disponible dans CADP. Dans le but d'améliorer les résultats de notre approche concernant le model checking, on explore des techniques d'abstraction dédiées aux systèmes d'information spécifiées en EB-3. En particulier, on se focalise sur une famille spécifique de systèmes qui s'appellent paramétriques dont le comportement varie en fonction de la valeur prédéfinie d'un paramètre du système. Enfin, on applique cette méthode dans le contexte de EB-3 / EB-3 is a specification language for information systems. The core of the EB-3 language consists of process algebraic specifications describing the behaviour of entities in a system, and attribute functions that are recursive functions evaluated on the system execution trace describing entity attributes. The verification ofEB-3 specifications against temporal properties is of great interest to users of EB-3. In this thesis, we focus on liveness properties of information systems, which express the eventuality that certain actions take place. The verification of liveness properties can beachieved with model checking. First, we present an operational semantics for EB-3 programs, in which attribute functions are computed during program evolution and their values are stored into program memory. This semantics permits us to define an automatic translation from EB-3 to LNT, a value-passing concurrent language with classical process algebra features. Our translation ensures the one-to-one correspondence between states and transitions of the labelled transition systems corresponding to theEB-3 and LNT specifications. Then, we automate this translation with the EB-3toLNT tool, thus equipping the EB-3 method with the functional verification features available in the model checking toolbox CADP. With the aim of improving the model checking results of this approach, we explore abstraction techniques for information systems specified inEB-3. In particular, we concentrate on a specific family of systems called parametric, whose behaviour is scaled in keeping with the predefined value of a system parameter. Finally, we apply this method on the EB-3 context

La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.

LNT est un langage formel de spécification récent, basé sur les algèbres de processus, où plusieurs processus concurrents et asynchrones peuvent interagir par rendez-vous multiple, c'est-à-dire à deux ou plus, avec échange de données. La boite à outils CADP (Construction and Analysis of Distributed Processes) offre plusieurs techniques relatives à l'exploration d'espace d'états, comme le model checking, pour vérifier formellement une spécification LNT. Cette thèse présente une méthode de génération d'implémentation distribuée à partir d'un modèle formel LNT décrivant une composition parallèle de processus. En s'appuyant sur CADP, nous avons mis au point le nouvel outil DLC (Distributed LNT Compiler), capable de générer, à partir d'une spécification LNT, une implémentation distribuée en C qui peut ensuite être déployée sur plusieurs machines distinctes reliées par un réseau. Pour implémenter de manière correcte et efficace les rendez-vous multiples avec échange de données entre processus distants, nous avons élaboré un protocole de synchronisation qui regroupe différentes approches proposées par le passé. Nous avons mis au point une méthode de vérification de ce type de protocole qui, en utilisant LNT et CADP, permet de détecter des boucles infinies ou des interblocages dus au protocole, et de vérifier que le protocole réalise des rendez-vous cohérents par rapport à une spécification donnée. Cette méthode nous a permis d'identifier de possibles interblocages dans un protocole de la littérature, et de vérifier le bon comportement de notre propre protocole. Nous avons aussi développé un mécanisme qui permet, en embarquant au sein d'une implémentation des procédures C librement définies par l'utilisateur, de mettre en place des interactions entre une implémentation générée et d'autres systèmes de son environnement. Enfin, nous avons appliqué DLC au nouvel algorithme de consensus Raft, qui nous sert de cas d'étude, notamment pour mesurer les performances d'une implémentation générée par DLC. / LNT is a recent formal specification language, based on process algebras, where several concurrent asynchronous processes can interact by multiway rendezvous (i.e., involving two or more processes), with data exchange. The CADP (Construction and Analysis of Distributed Processes) toolbox offers several techniques related to state space exploration, like model checking, to formally verify an LNT specification. This thesis introduces a distributed implementation generation method, starting from an LNT formal model of a parallel composition of processes. Taking advantage of CADP, we developed the new DLC (Distributed LNT Compiler) tool, which is able to generate, from an LNT specification, a distributed implementation in C that can be deployed on several distinct machines linked by a network. In order to handle multiway rendezvous with data exchange between distant processes in a correct and efficient manner, we designed a synchronization protocol that gathers different approaches suggested in the past. We set up a verification method for this kind of protocol, which, using LNT and CADP, can detect livelocks or deadlocks due to the protocol, and also check that the protocol leads to valid interactions with respect to a given specification. This method allowed us to identify possible deadlocks in a protocol from the literature, and to verify the good behavior of our own protocol. We also designed a mechanism that enables the final user, by embedding user-defined C procedures into the implementation, to set up interactions between the generated implementation and other systems in the environment. Finally, we used the new consensus algorithm Raft as a case study, in particular to measure the performances of an implementation generated by DLC.

Cette thèse s'intéresse à l'étude des méthodes formelles de spécification et de vérification dans le cadre des systèmes d'information. Les systèmes d'informations sont des systèmes dynamiques constitués d'entités et d'associations représentées par la composition en parallèle de processus répliqués issus de différentes classes. De plus, ces systèmes font partie de la classe des systèmes paramétrés. On propose un modèle de spécification de systèmes paramétrés, nommé PASTD, qui est adapté aux systèmes d'information et qui est basé sur la notation des diagrammes états-transitions algébriques (ASTD). Puis, on étudie le problème de sûreté pour les PASTD, à travers la méthode de vérification de couverture pour les systèmes de transitions bien structurés (WSTS). Cette méthode repose sur trois conditions principales : la monotonie, le beau préordre et la pred-base effective. Les PASTD sont montrés comme étant monotones et on définit une sous-classe vérifiant la propriété de beau préordre. Enfin, on décrit une nouvelle méthode, adaptée aux systèmes paramétrés, qui explicite un ensemble de conditions permettant de prouver la pred-base effective. Ces conditions définissent une nouvelle classe appelée RMTS (\emph{Ranked Monotone Transition Systems}). Cette méthode est appliquée aux PASTD.

Les réseaux ad hoc dynamiques qui évoluent de manière non planifiée et imprévisible sont souvent étudiés en faisant l’hypothèse d’une composition et d’une topologie qui évoluent peu et relativement lentement. Il est alors possible de proposer dans ce contexte faiblement mobile des mécanismes (comme par exemple du routage, des infrastructures PKI, etc.) qui permettent aux applications conçues pour les réseaux statiques de continuer à fonctionner. Les travaux présentés dans cette thèse sont au contraire centrés sur lesréseaux ad hoc fortement dynamiques (iMANets). Les nœuds qui les constituent sont extrêmement mobiles et volatils, ce qui engendre des modifications incessantes et rapides de topologie. Les contributions principales de cette thèse sont (i) la définition d’une algèbre nommée CiMAN (Calculus for highly Mobile Ad hoc Networks) qui permet de modéliser les processus communicants dans ces réseaux ad hoc fortement mobiles, (ii) l’utilisation de cette algèbre pour prouver la correction d’algorithmes dédiés à ces réseaux, et (iii) unmiddleware et des applications de référence adaptés à ce contexte. / Mobile ad hoc networks that evolve in an unplanned and unpredictable mannerare often studied assuming that their composition and their topology evolve relatively slowly. In this context of weak mobility, it is then possible to propose mechanisms (such asrouting, Public Key Infrastructure, etc.) which make the application designed for a static context still operational. At the opposite, the work presented in this thesis focuses on highlymobile ad hoc networks (iMANets). The nodes of these networks are extremely mobile,bringing ceaseless and fast changes in the network topology. The main contributions of this thesis are (i) the definition of an algebra called CiMAN (Calculus for highly Mobile Adhoc Networks) which makes it possible to model communicating processes in these highly mobile ad hoc networks, (ii) the use of this algebra to prove the correctness of algorithms dedicated to these networks, and (iii) a middleware and reference applications specifically designed for this context.

.

La validation, incluant vérification fonctionnelle et évaluation de performance, est un processus critique pour la conception de designs matériels complexes : un design fonctionnellement correct peut s'avérer incapable d'atteindre la performance ciblée. Plus un problème dans un design est identifié tard, plus son coût de correction est élevé. La validation de designs devrait donc être entreprise le plus tôt possible dans le flot de conception. Cette thèse présente un formalisme de modélisation par composition, couvrant les aspects fonctionnels et temporisés des systèmes matériels, et définit une approche d'évaluation de performance afin d'analyser les modèles construits. Le formalisme de modélisation défini, appelé Interactive Probabilistic Chain (IPC), est une algèbre de processus a temps discret. Nous avons défini une bisimulation de branchement et prouvé sa congruence par rapport à l'opérateur de composition parallèle, nous permettant une approche compositionnelle. les IPCs peuvent être vues comme une transposition des Interactive Markov Chains dans un espace de temps discret. Pour l'évaluation de performance, une IPC complètement spécifiée est transformée en une chaîne de Markov à temps discret, qui peut être analysée. De plus, nous avons défini une mesure de perfor- mance, appelée latence, et un algorithme permettant de calculer sa distribution moyenne sur le long terme. A l'aide d'outils permettant de traiter les IPCs, développés sur la base de la boîte à outils CADP, nous avons étudié les aspects de communication d'un design industriel, l'architecture xSTream, développée chez STMicroelectronics.