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.
| Identifer | oai:union.ndltd.org:usherbrooke.ca/oai:savoirs.usherbrooke.ca:11143/11630 |
| Date | January 2018 |
| Creators | Chane-Yack-Fa, Raphaël |
| Contributors | Frappier, Marc, Mammar, Amel |
| Publisher | Université de Sherbrooke |
| Source Sets | Université de Sherbrooke |
| Language | French, English |
| Detected Language | French |
| Type | Thèse |
| Rights | © Raphaël Chane-Yack-Fa, Attribution - Pas d’Utilisation Commerciale - Partage dans les Mêmes Conditions 2.5 Canada, Attribution - Pas d’Utilisation Commerciale - Partage dans les Mêmes Conditions 2.5 Canada, http://creativecommons.org/licenses/by-nc-sa/2.5/ca/ |
Page generated in 0.002 seconds