Qualité de service dans une logique temporelle compositionnelle
Abstract
Non disponible / Not available
Ces dernières années ont donné lieu a un développement conséquent des
moyens de télécommunication. Une architecture physique en constante évolution
a entraîné la mise au point de services de plus en plus nombreux et de
plus en plus sophistiqués. Par ailleurs, le nombre de prestataires de tels services
s'est aussi accru. Les systèmes de télécommunication sont donc de plus en
plus performants, mais aussi de plus en plus compliqués. Obtenir une certaine
garantie de leur correction n'est donc plus aussi simple qu'avant.
Le but de notre étude était double : il s'agissait d'offrir un moyen permettant
d'effectuer certaines vérifications sur le comportement du système par
rapport à des propriétés spécifiées formellement, tout en permettant l'écriture
indépendante de spécifications de services devant par la suite fonctionner ensemble. À l'issue d'une étude de cas, nous avons décrit des opérateurs de composition et des règles de preuve associées permettant de composer de manière sûre des services, sans devoir modifier les spécifications initiales.
Pour supporter les principes de composition ainsi définis, nous avons décidé,
pour spécifier les services de télécommunication, de définir une surcouche à la
méthode B, permettant de spécifier des propriétés temporelles sur un système
d'actions tout en gardant des caractéristiques intéressantes de B telles que
l'existence d'outils performants. Le langage que nous avons défini a été construit sur le principe de la programmation littéraire. Cela permet une meilleure traçabilité entre cahier des charges et spécification formelle, ainsi qu'une génération automatique d'une partie du développement formel. Par ailleurs, la structuration forte de notre langage nous a permis de définir une méthodologie pour le développement de services de l'initiateur du projet jusqu'à la personne chargée de la validation de la spécification formelle obtenue.