Modélisation et validation des systèmes informatiques

Modélisation et validation des systèmes informatiques

La modélisation est une étape importante dans la conception d’un système, vu la complexité et contraintes temps/développement de sa conception matérielle. Une conception incorrecte d’un système hardware complexe est très coûteuse, c’est pourquoi, les concepteurs ont recours à des techniques de vérification dès les premières phases du flot de conception.

Plusieurs techniques existent. On retrouve des techniques basées sur les méthodes analytiques, la vérification formelle ou la simulation. Cette dernière a été retenue pour les travaux de cette thèse. La modélisation d’un système consiste à spécifier un modèle qui reproduit son comportement. Ce modèle est une abstraction plus ou moins précise d’un système réel. En fonction du degré d’abstraction, on obtient un modèle plus ou moins fidèle. Dans ce qui suit, nous présentons les trois techniques de vérification citées ci-dessus. 

Validation par méthodes analytiques

Les méthodes analytiques proposent d’étudier le comportement stationnaire d’un système en résolvant son modèle mathématique, ou plus précisément, en résolvant les équations mathématiques sous-jacentes à son modèle mathématique [Maria, 1997]. L’intérêt des méthodes analytiques réside principalement dans la résolution des équations généralement peu coûteuse en temps de calcul. Leur inconvénient est qu’il est généralement nécessaire de faire des hypothèses restrictives sur le système réel pour pouvoir obtenir des modèles exploitables. 

Validation par vérification formelle

Il s’agit de méthodes basées sur des preuves mathématiques sur la validité de la conception d’un système [Swan, 2006]. La vérification formelle d’un système nécessite les descriptions formelles de la conception et de la spécification. En pratique, ces méthodes sont efficaces sur des systèmes à états finis de tailles moyennes. Dans ce qui suit, nous citons deux méthodes de vérification formelle. 64 Méthodologie de vérification Vérification formelle par l’algèbre des processus Il s’agit d’une famille de formalismes proposée par la théorie de la concurrence. Un processus représente le comportement d’un système qui regroupe un ensemble d’évènements ou d’actions que ce système peut réaliser et l’ordre de leur exécution [Biemans and Blonk, 1986].

L’algèbre des processus fournit une description des interactions, des communications et des synchronisations entre un ensemble de composants indépendants du système concurrent. Des lois sont définies pour décrire, manipuler et analyser les différents processus. Le langage LNT (LOTOS New Technology) est un langage de spécification moderne qui regroupe les caractéristiques de l’algèbre des processus et un ensemble de définitions des processus (process par exemple) et de définitions de types (type ou endtype) [Dwyer et al., 1999]. Dans [Park, 2007], plusieurs exemples sont donnés sur la vérification des systèmes numériques en utilisant l’algèbre des processus.