Institut d'Informatique

Projet: Outils pour l'ingéniérie des besoins de systèmes composites

Project: Tools for the Requirements Engineering of Composite Systems

Description:

Français:

Principalement dans le cadre des projets Région Wallonne/Objectif 1 CAT et du projet Esprit CREWS, nous sommes en train de développer un environnement intégré d'outils destinés à supporter le langage ALBERT.

Le développement de ces outils repose sur une architecture de type client/serveur. La partie client est constituée d'un éditeur graphique et textuel s'exécutant sur une plateforme Windows 95/NT. La partie serveur est constituée d'outils supportant des activités plus complexes. Ces outils s'interfacent au travers d'une structure d'accueil (le "repository" ConceptBase) et tournent sur une platforme UNIX.

Les outils actuellement disponibles permettent des contrôles syntaxiques poussés ainsi que certains contrôles sémantiques élémentaires. Les fonctionnalités d'outils plus sophistiqués pour la vérification et la validation ont été identifiées. Au niveau vérification, nous utilisons le système de preuves PVS (voir Unité Sémantique, Logique et Calcul) et développons un niveau d'interface autour de celui-ci permettant de fournir plus d'assistance à l'analyste dans son élaboration et son exécution d'une preuve. Au niveau validation, nous avons étudié les fonctionnalités d'un paraphraseur ainsi que d'un système permettant d'assurer, dans model distribué, l'animation, au niveau symbolique, d'une spécification Albert.

English

Mainly within the framework of the Walloon Region/Objetcif 1 CAT project and the Esprit CREWS project, we are developing an integrated environment of tools for supporting the ALBERT language.

The general architecture of the tool is based on a client/server arhcitecture where (i) the client is made of a graphical/textual editor running on top of a Windows 95/NT platform (ii) the server is based on set of a more complex tools developed in Unix around a repository (ConceptBase) structure.

Basic tools related to syntactic and basic semantic checks have been developed. Besides them, more advanced tools are being investigated related to verification and validation of Albert specifications. At the verification level, we use the PVS system for dealing with detailed formal proofs (see Unité Sémantique, Logique et Calcul) and develop a higher level interface allowing the analyst to be guided in his/her elaboration and performance of the proof. At the validation level, we have investigated the functionalities of a paraphraser as well as of an animator allowing to support a cooperative and distributed symbolic execution of an Albert specification.

Responsables

• Eric DUBOIS Chargé de cours
  

Composition

Mots Clés / Keywords

specification editor, syntax and semantic checkers, repository, theorem prover, high-level proof, animator/simulator

Plan / Schedule

FUNDP Institut d'Informatique

---