Abstract FR:

L'emploi des specifications formelles est d'une grande importance, tout particulierement pour le developpement de systemes dits securitaires ou critiques. Les specifications mixtes ont pour but de permettre l'expression des differents aspects que peuvent presenter ces systemes : statique (types de donnee), dynamiques (comportements) et composition (architecture, concurrence et communication). La complexite des systemes de taille reelle rend indispensable la definition de moyens de structuration des specifications mixtes. Pour cela, nous proposons un modele base sur une hierarchie de structures que nous appelons vues, ainsi que korrigan, le langage formel associe. Les vues integrent des systemes de transition symboliques, des specifications algebriques et une forme de logique temporelle. Elles permettent la specification des differents aspects de facon unifiee. Elles sont expressives, lisibles et favorisent la definition de composants a un haut niveau d'abstraction. Notre modele offre trois moyens de structuration des specifications. La structuration interne permet de definir les aspects de base des composants (dynamique et statique). La structuration externe permet de definir de facon unifiee differents types de compositions : tant l'integration d'aspects que la composition concurrente de composants communicants. Une forme simple de structuration d'heritage permet de reutiliser les composants. Nous pensons qu'il est important, pour que les methodes formelles soient reellement utilisees, qu'elles disposent d'une methode associee. Dans cette optique, nous proposons une methode pour la specification mixte et structuree, applicable aux specifications korrigan ainsi qu'a d'autres formalismes. Enfin, nous proposons un atelier, ask, dedie a la specification mixte en korrigan. Il integre des mecanismes de verification des specifications korrigan par traduction et de generation de code oriente-objet.