| Le développement des
réseaux d'ordinateurs permettant l'interconnexion de machines
se poursuit. Aussi les questions posées par la construction du logiciel
pour ces systèmes sont d'une grande actualité. Même
si des progrès spectaculaires ont été accomplis dans
les méthodes de génie logiciel, le caractère intrinsèquement
parallèle et réparti des logiciels mis en oeuvre continue
à poser des problèmes ardus de programmation.
La question la plus sensible à nos yeux est celle de la maîtrise
de la fiabilité du logiciel, c'est-à-dire le contrôle
des conditions de son bon fonctionnement. La maîtrise
du développement passe par le renforcement des activités
de conception, validation et test.
Du point de vue de la conception, la priorité
est donnée aux environnements de conception objet
et à l'invention de "frameworks" spécialisés
pour les systèmes communicants et intégrant des outils de
validation.
Du point de vue de la validation, l'idée est
de renforcer l'impact des méthodes formelles et des
outils d'analyse pour permettre la mise au point des spécifications
et la génération de tests pour les codes répartis.
L'approche du projet Pampa consiste à
contribuer à l'élaboration de nouvelles technologies
logicielles par l'étude de modèles formels des protocoles
et l'invention d'outils informatiques associés. Nous
privilégions la conception d'outils automatiques permettant d'aider
aux tâches de conception, vérification, génération
de code et test de programmes réels. Ces outils ont vocation à
être diffusés dans le milieu académique et/ou industriel.
La mise au point des modèles et outils s'effectue
dans le cadre d'applications réparties situées principalement
dans le domaine du logiciel pour les télécommunications.
Le fonds scientifique du projet est constitué des méthodes
formelles en logiciel de télécommunication, des techniques
du type "model-checking" fondées sur des parcours
de systèmes de transitions, des méthodes de conception
objet et des techniques de distribution de code.
L'activité scientifique du projet peut être structurée
en trois thèmes de recherche :
- vérification et test des programmes répartis,
- méthodes et modèles pour le logiciel objet réparti,
- nouveaux modèles pour les logiciels de télécommunications.
La vérification et le
test des programmes répartis :
La vérification consiste à s'assurer, qu'avant toute implantation,
l'application se comportera correctement. Cette question revêt une
importance particulière pour les programmes répartis, compte-tenu
de la complexité des comportements qu'ils engendrent. Elle est essentielle
pour les logiciels critiques. L'activité de vérification
est complétée par le test de la conformité des implantations.
Nous nous concentrons sur les techniques par modèles (dites «model-checking»),
et particulièrement sur les aspects algorithmiques (algorithmique
à la volée). Nous avons étendu ces techniques pour
être capable de générer automatiquement des séquences
de test de conformité pendant la vérification des programmes,
spécifiés dans des langages comme SDL ou LOTOS. Cela a conduit
à un outil original par son algorithmique et son architecture (appelé
TGV), que nous valorisons auprés de la société Vérilog.
Un autre aspect du test est l'évaluation des comportements d'un
code réparti à partir des traces qu'il produit. Pour modéliser
les phénomènes de causalité et de concurrence, la
théorie de l'ordre est notre outil mathématique de base.
Nous avons plusieurs applications comme la détection au vol de propriétés,
le test d'interopérabilité et le diagnostic de pannes dans
les réseaux. Enfin, pour qu'elle ait un véritable impact,
la validation (vérification/test) doit s'intégrer dans des
environnements et méthodes de conception existantes. Pour cela,
le paradigme objet et la notation UML sont maintenant incontournables.
Méthodes et modèles
pour le logiciel objet réparti :
Une question scientifique difficile est d'être capable de construire
des architectures logicielles fiables et efficaces, tout en prenant en
compte les problèmes liés au parallélisme et à
la répartition. Notre approche, fondée sur l'idée
de réutilisation de solutions éprouvées, est l'identification
de modèles spécifiques pour des domaines d'applications (exemple
du modèle SPMD pour le calcul réparti ou de CORBA pour les
objets télécoms), et la définition de cadres de conception,
de réalisation et de validation adaptés à ces modèles
(«frameworks», «design patterns»).
Nouveaux modèles pour
les logiciels de télécommunications :
La validation de logiciels objet, la nécessité de raisonner
formellement sur des spécifications de plus en plus haut niveau
et hétérogènes, nous conduisent à proposer
de nouveaux modèles sémantiques qui pourront ensuite se prêter
à des analyses ou transformations. Nous nous focalisons sur les
aspects comportementaux des modèles que l'on représente par
des familles d'ordres partiels. Nous proposons le formalisme BDL, en collaboration
avec le projet EP-ATR pour étudier une sémantique mixte synchrone-asynchrone
pour pouvoir faire bénéficier les systèmes répartis
asynchrones de la technologie de compilation synchrone. L'analyse des MSC,
l'analyse MaxPlus font partie des réflexions de ce thème
amont qui a vocation à préparer les prototypes de demain.
UML joue le rôle d'une notation fédératrice. |
