Retour au site du LAAS-CNRS

Résumé

Les systèmes temps réel et distribués posent des problèmes complexes en termes de conception darchitecture et de description de comportements. De par leur criticité en vies humaines et leurs coûts de prototypage, ces systèmes ont motivé le développement dune activité de recherche sur les langages de modélisation formelle et les techniques de validation basées modèle qui contribuent à la détection au plus tôt des erreurs de conception. Néanmoins, les langages formels ont eu un succès plus que limité dans lindustrie. Larrivée du langage UML (Unified Modeling Language) a ouvert de nouveaux horizons pour lintégration de langages de modélisation formelle dans une méthodologie de conception susceptible dêtre mieux acceptée par les praticiens du domaine. En sappuyant sur une expérience antérieure de la technique de description formelle Estelle et des extensions temporelles des réseaux de Petri, notre activité de recherche sur les cinq dernières années a débouché sur la production dun profil UML nommé TURTLE (Timed UML and RT-LOTOS Environment). TURTLE surpasse UML 2.0 par ses extensions aux diagrammes danalyse et de conception UML, sa sémantique formelle exprimée en RT-LOTOS, et ses outils de support (éditeur de diagrammes et outil de validation formelle combinant simulation et vérification basée sur une analyse daccessibilité). La méthodologie TURTLE trouve son champ dapplication naturel dans la conception de systèmes temps réel et la validation darchitectures de communication en particulier. Lapproche proposée a été appliquée avec succès à des systèmes satellitaires et des protocoles dauthentification.

Abstract

Real-time and distributed systems capture complex problems in terms of architecture design and behavior description. Because of their life-criticality and prototyping costs, these systems have stimulated research work on formal modeling language and model-based validation techniques that enable early detection of design errors. Nevertheless, formal modeling languages have incompletely succeeded in industry. The advent of the OMG-based Unified Modeling Language (UML) has open new avenues for an integration of formal modeling languages into a design methodology that might receive greater acceptance among practitioners. Relying on former experience with the formal description technique Estelle and timed extensions of Petri Nets, the main output of our research activity over the last five years is a real-time UML profile named TURTLE (Timed UML and RT-LOTOS Environment). TURTLE supersedes UML 2.0 by its extension of UML analysis and design diagrams, its formal semantics expressed in RT-LOTOS, and its toolkit (diagram editor and formal validation tool combining simulation capabilities and verification based on reachability analysis). The TURTLE methodology typically applies to real-time system design and communication architecture validation. This approach has been successfully applied on space-based systems and authentication protocols.

Mots-Clés / Keywords

Modélisation; Systèmes temps réel; Systèmes distribués; UML; RT-LOTOS; Validation formelle; Modeling; Real-time systems; Distributed systems; Formal validation;