Une approche de vérification formelle et de simulation pour les systèmes à événements : application à PROMELA

• Main Author: Yacoub, Aznam
• Other Authors: Aix-Marseille
• Language: en
• Published: 2016
• Subjects: Vérification et Validation; Modélisation et Simulation; Systèmes à Evènements Discrets; Méthodes Formelles; Systèmes temporisés; Promela; DEv-PROMELA; Verification and Validation; Modeling and Simulation; Discrete-Event Systems; Formal Methods; Timed Systems
• Online Access: http://www.theses.fr/2016AIXM4373/document

De nos jours, la mise au point de logiciels ou de systèmes fiables est de plus en plus difficile. Les nouvelles technologies impliquent de plus en plus d'interactions entre composants complexes, dont l'analyse et la compréhension deviennent de plus en plus délicates. Pour pallier ce problème, les domaines de la vérification et de la validation ont connu un bond significatif avec la mise au point de nouvelles méthodes, réparties en deux grandes familles : la vérification formelle et la simulation. Longtemps considérées comme à l'opposée l'une de l'autre, les recherches récentes essaient de rapprocher ces deux grandes familles de méthodologies. Dans ce cadre, les travaux de cette thèse proposent une nouvelle approche pour intégrer la simulation dites à évènements discrets aux méthodes formelles. L'objectif est d'améliorer les méthodes formelles existantes, en les combinant à la simulation, afin de leur permettre de détecter des erreurs qu'elles ne pouvaient déceler avant, notamment sur des systèmes temporisés. Cette approche nous a conduit à la mise au point d'un nouveau langage formel, le DEv-PROMELA. Ce nouveau langage, créé à partir du PROMELA et du formalisme DEVS, est à mi-chemin entre un langage de spécifications formelles vérifiables et un formalisme de simulation. En combinant alors un model-checking traditionnel et une simulation à évènements discrets sur le modèle exprimé dans ce nouveau langage, il est alors possible de détecter et de comprendre des dysfonctionnements qu'un model-checking seul ou qu'une simulation seule n'auraient pas permis de trouver. Ce résultat est notamment illustré à travers les différents exemples étudiés dans ces travaux. === Nowadays, making reliable software and systems is become harder. New technologies imply more and more interactions between complex components, whose the analysis and the understanding are become arduous.To overcome this problem, the domains of verification and validation have known a significant progress, with the emergence of new automatic methods that ensure reliability of systems. Among all these techniques, we can find two great families of tools : the formal methods and the simulation. For a long time, these two families have been considered as opposite to each other. However, recent work tries to reduce the border between them. In this context, this thesis proposes a new approach in order to integrate discrete-event simulation in formal methods. The main objective is to improve existing model-checking tools by combining them with simulation, in order to allow them detecting errors that they were not previously able to find, and especially on timed systems. This approach led us to develop a new formal language, called DEv-PROMELA. This new language, which relies on the PROMELA and on the DEVS formalism, is like both a verifiable specifications language and a simulation formalism. By combining a traditional model-checking and a discrete-event simulation on models expressed in DEv-PROMELA, it is therefore possible to detect and to understand dysfunctions which could not be found by using only a formal checking or only a simulation. This result is illustrated through the different examples which are treated in this work.