Qualité de service dans une logique temporelle compositionnelle

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.Non disponible / Not availabl