Show simple document record

dc.contributor.advisorFrappier, Marc
dc.contributor.advisorMammar, Amel
dc.contributor.authorChane-Yack-Fa, Raphaëlfr
dc.date.accessioned2018-01-10T14:21:47Z
dc.date.available2018-01-10T14:21:47Z
dc.date.created2018fr
dc.date.issued2018-01-10
dc.identifier.urihttp://hdl.handle.net/11143/11630
dc.description.abstractCette 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.fr
dc.language.isofrefr
dc.language.isoengfr
dc.publisherUniversité de Sherbrookefr
dc.rights© Raphaël Chane-Yack-Fafr
dc.rightsAttribution - Pas d’Utilisation Commerciale - Partage dans les Mêmes Conditions 2.5 Canada*
dc.rightsAttribution - Pas d’Utilisation Commerciale - Partage dans les Mêmes Conditions 2.5 Canada*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/2.5/ca/*
dc.subjectVérification paramétréefr
dc.subjectModel checkingfr
dc.subjectSystème d'informationfr
dc.subjectAlgèbre de processusfr
dc.subjectAutomatefr
dc.subjectSystème de transitions bien structuréfr
dc.subjectBeau préordrefr
dc.subjectCouverturefr
dc.subjectSûretéfr
dc.subjectAccessibilitéfr
dc.titleVérification formelle de systèmes d'informationfr
dc.typeThèsefr
tme.degree.disciplineInformatiquefr
tme.degree.grantorFaculté des sciencesfr
tme.degree.levelDoctoratfr
tme.degree.namePh.D.fr


Files in this document

Thumbnail
Thumbnail

This document appears in the following Collection(s)

Show simple document record

© Raphaël Chane-Yack-Fa
Except where otherwise noted, this document's license is described as © Raphaël Chane-Yack-Fa