|
Le thème de recherche central du projet COLOSS est la conception d'outils d'aide au développement et à la validation de composants logiciels. Notre approche est fondée sur une expérience collective sur les thèmes des méthodes formelles, de l'intégration des paradigmes, de l'analyse et conception objet et de la validation. Dans le présent projet, nous nous attelons à l'étude et à l'élaboration de concepts, mécanismes et outils pour modéliser et développer des composants et des logiciels sûrs. La modélisation (on parle aussi de spécification) est une démarche scientifique qui consiste, pour des fins d'étude, à élaborer une abstraction d'un phénomène ou d'un système. On peut modéliser un système existant, ou bien modéliser un système à construire.Un composant est une entité logicielle dotée d'une spécification précise, d'un fonctionnement précis et d'une interface permettant de l'utiliser dans la construction d'autres logiciels. Nous adoptons la vision module réutilisable (Parnas}, reprise par exemple dans les travaux de Meyer (Trusted Components). Par sûreté nous entendons un fonctionnement correct c'est-à-dire tel qu'il est prévu par les spécifications informelles puis les spécifications formelles. La modélisation et la technologie des composants font l'objet de nombreuses études depuis plusieurs années. Cependant de nombreux problèmes demeurent; par exemple la construction de modèles mathématiquement corrects, la construction de composants dont le fonctionnement est sûr, la preuve de correction des propriétés attendues des composants, la réutilisation des composants, les méthodes rigoureuses d'élaboration et de composition de composants, la validation d'une spécification du composant par le client, l'utilisation de plusieurs paradigmes dans un composant, etc. Les problèmes ou questions ouvertes sont de différents types :
Les travaux abordés dans notre projet sont des préoccupations importantes identifiées clairement en génie logiciel (software engineering). Ils se situent à la frontière entre les travaux purement théoriques et les travaux plus technologiques. Ceci est en soit une de nos originalités ; en effet, les groupes de recherche se situent souvent dans une des communautés. Dans le but de réduire les coûts de conception et de maintenance des systèmes informatiques, de rendre leur fonctionnement plus sûr et de satisfaire à certaines normes pour la certification, l'utilisation de méthodes formelles et semi-formelles pour les spécifier et les vérifier est devenue nécessaire. Cependant, tous les aspects d'un système informatique ne pouvant ni être spécifiés, ni être vérifiés avec une seule approche, l'utilisation conjointe de différentes approches doit être envisagée. Cette problématique est une des préoccupations essentielles dans la communauté internationale du génie logiciel et de la conception de circuits digitaux. Notre objectif est de résoudre des problèmes
théoriques liés, d'une part à la cohabitation de
modules de spécifications écrits avec des
formalismes différents, et d'autre part à l'utilisation
conjointe de techniques de vérifications différentes. Ces
travaux s'organiseront autour de la conception d'un environnement
performant de spécification, de vérification et de
développement. Cet environnement permettra d'intégrer
des spécifications écrites avec des
méthodes/langages différents, de les valider et de les
vérifier à l'aide de différentes techniques.
L'environnement devra aussi permettre la génération
de code en langage orienté objet. |