<  Back to the Polytechnique Montréal portal

Model-Checking symbolique pour la vérification de systèmes et son application aux tables de décision et aux systèmes d'éditions collaboratives distribuées

Manal Najem

Master's thesis (2009)

Open Access document in PolyPublie
[img]
Preview
Open Access to the full text of this document
Terms of Use: All rights reserved
Download (7MB)
Show abstract
Hide abstract

Abstract

Verification is one crucial activity in any software life cycle. Its major role is to ensure anidentification of potential design and implementation flaws integrated in the software systemduring its development process. Such an identification leads to eventual corrections in theearly steps of the development cycle, thus avoiding tedious work otherwise required in thesystem requirements' reanalysis as well as in its remodelling preceding its deployment. As aconsequence, the verification step is rigorously put into practice through formal methodsand tools. Given such a formalisation contributes to give another level of insurance to boththe system's designers and users.This thesis is related to a research which aims at applying one specific formal method inprogram and requirements analysis: symbolic execution intertwined with model checking.This technique has known a major development in the past few years, thus raising interestamong researchers in the field.On one hand, symbolic execution explores all possible execution paths of a programmodelling a system using uninitialised input variables. As its name implies, this specificexecution deals with abstract or "symbolic" variables. Hence, those visited pathscharacterise the abstract program behaviour. On another hand, model checking ensures asystematic exploration of those different execution paths through an exhaustive visit of allreachable states. This approach is necessary for subsequent generation of counterexamplesin case of property violations within the system.Therefore, symbolic execution along with model checking is a resulting approach enforcedwith advantages of both techniques. This yields a higher degree of interpreting the retrievedflaws provided through generated counterexamples, for even the most sophisticatedsystems.

Résumé

Dans le cycle de vie de tout système logiciel, une phase cruciale de formalisation et devalidation au moyen de vérification et/ou de test induit une identification d'erreurs probablesinfiltrées durant sa conception. Cette détection d'erreurs et leur correction sontavantageuses dans les premières phases de développement du système afin d'éviter toutretour aux travaux ardus d'analyse de spécifications et de modélisation du systèmeprécédant sa réalisation. Par conséquent, cette étape mise en oeuvre à travers desméthodes et des outils formels dans les phases amont de la conception contribue àaugmenter la confiance des concepteurs et utilisateurs vis-à-vis de la fonctionnalité dusystème.L'objectif de cette maîtrise s'insère dans le cadre d'une recherche qui vise à exploiter unetechnique formelle spécifique d'analyse de programmes et de spécifications: l'exécutionsymbolique combinée au model-checking. Cette technique représente une approcheémergente à laquelle les chercheurs ont porté une attention particulière ces dernièresannées.D'une part, l'exécution symbolique permet d'explorer les chemins d'exécution possibles d'unprogramme modélisant un système avec des variables d'entrée non initialisées, en d'autrestermes en manipulant des variables abstraites ou "symboliques". Ces chemins caractérisentainsi le comportement du programme de manière abstraite. D'autre part, le model-checkingpermet d'explorer systématiquement ces différents chemins d'exécution à l'aide d'uneénumération exhaustive des états accessibles afin de générer ultérieurement des contreexemplesen cas de violation de propriétés du système.De ce fait, l'exécution symbolique combinée au model-checking englobe les points forts deces deux techniques octroyant aux concepteurs du système une compréhension accrue dessituations d'erreur dans les contre-exemples ainsi générés.
Department: Department of Computer Engineering and Software Engineering
Program: Génie informatique
Academic/Research Directors: Hanifa Boucheneb, Ettore Merlo
PolyPublie URL: https://publications.polymtl.ca/140/
Institution: École Polytechnique de Montréal
Date Deposited: 16 Nov 2009 14:16
Last Modified: 09 Nov 2022 09:55
Cite in APA 7: Najem, M. (2009). Model-Checking symbolique pour la vérification de systèmes et son application aux tables de décision et aux systèmes d'éditions collaboratives distribuées [Master's thesis, École Polytechnique de Montréal]. PolyPublie. https://publications.polymtl.ca/140/

Statistics

Total downloads

Downloads per month in the last year

Origin of downloads

Repository Staff Only

View Item View Item