ORGANISER LES CONNAISSANCES ET
LES INTERACTIONS

Une profusion d’informations Informations hétérogènes 

Un processus de conception et vérification par model checking produit une profusion d’informations hétérogènes (spécifications, modèles structurels ou comportementaux, propriétés, traces …), et ce à différents niveaux d’abstractions et de détails, comme argumenté par [RB03]. Dans le chapitre 4, nous avons vu par exemple qu’une des techniques de diagnostic consistait à écrire un ensemble de propriétés liées à des connaissances en model checking. Cette technique produisait 30 propriétés pour un système très simple. Aussi pour faciliter leur mise en œuvre et limiter les erreurs, ces propriétés doivent être générées (conformément à des normes de nommage) ou instanciées à partir d’un modèle ou d’un patron défini par un expert, et dont les concepts doivent être formalisés. Ces modèles peuvent être stockés dans une bibliothèque. Relations Des relations de tout ordre existent entre ces informations. Dans le chapitre 5, par exemple, nous avons vu que pour résoudre le fossé sémantique il fallait rapprocher deux types de connaissances, les connaissances du niveau domaine et les connaissances liées au model checking. Pour cela il s’agit de définir des corrélations entre ces éléments. Pour pouvoir outiller ces corrélations, celles-ci doivent être capturées et formalisées. Temporalité Ces informations et leurs relations évoluent au cours du temps. Elles sont modifiées, enrichies ou abandonnées tout au long du processus de conception et de vérification. Dans le chapitre 5, nous avons vu par exemple qu’un processus de résolution de problèmes  implique une multitude de cycles de conception-vérification. Lors de ces cycles, des solutions sont produites, conservées, améliorées ou bien abandonnées. Le système devient au fil du temps un enchevêtrement de solutions (associées à leurs problèmes) garantissant des propriétés. Si l’on ne conserve pas l’historique de ces solutions, ont perd alors les raisonnements qui nous ont conduits à ces solutions. 

Besoin de gérer le processus de vérification

Constat actuel sur la gestion du processus de vérification Actuellement on constate que les processus de vérification font face aux problèmes suivants : – (1) Les connaissances ne sont pas bien gérées, et donc indisponibles. – (2) Les activités manipulant ces connaissances ne sont pas bien contrôlées, ni enregistrées. – (3) Il n’y a pas de consensus sur un formalisme de ces connaissances. – (4) Il n’y a pas d’accord sur une manière de les capturer. Pour capturer et utiliser les connaissances et les relations au fil du temps, il faut une gestion du processus de vérification qui n’est aujourd’hui pas pratiquée [RB03]. 

Vers un système organisationnel 

Baier souligne que, de manière transversale aux autres phases, le processus de vérification doit être planifié, administré et organisé, à travers une activité appelée l’organisation de la vérification [BK08]. Un système supportant l’organisation de la vérification serait aussi en mesure de capitaliser les expériences passées, et d’en permettre la réutilisation, notamment pour contribuer au processus de diagnostic. L’enjeu de ce chapitre est de proposer une infrastructure pour organiser ces connaissances et les interactions qu’elles supportent. Pour cela, il faut répondre à différentes questions : – (1) Où et sous quelle forme capturer ces éléments ? – (2) Comment les retrouver et quelles sont les interactions possibles ? 

Système organisationnel

 Organiser, c’est créer des capacités en imposant intentionnellement un ordre et une structure [Glu12]. C’est une activité tellement commune que nous le faisons souvent inconsciemment (organiser les jouets dans des boîtes, organiser les vêtements dans les placards…). Ces tâches organisatrices ne sont souvent pas réfléchies ou exprimées. Nous prenons pour acquis les concepts et les méthodes utilisés dans le système d’organisation 128 7.1. Introduction avec lequel nous travaillons. Dans [Glu12], Glushko introduit le concept de système organisationnel qu’il définit comme « un ensemble de ressources organisé intentionnellement et les interactions qu’elles supportent ». La figure 7.1 décrit un modèle conceptuel d’un tel système découpé en trois parties : – (1) Les ressources disposées intentionnellement – (2) Les différentes interactions (différents types de flèches) – (3) Les entités (humaines ou machines) qui interagissent avec les ressources dans différents contextes. Une ressource est une chose physique (un fichier de trace) ou non physique (le concept de configuration), ou une information sur cette chose (ce fichier de trace représente un contre-exemple). Une collection est une ressource qui regroupe des ressources sélectionnées dans un but (ce run de vérification vérifie la propriété P RT1 sur le modèle System1). Un arrangement intentionnel met l’accent sur l’organisation explicite ou implicite commis par des personnes (ou processus), se différenciant des disposition naturelles (créés par des processus physiques ou temporels). Une interaction est une action, une fonction, un service ou une capacité qui utilise les ressources d’une collection ou de la collection dans son ensemble.