 |
|  |
|
| |
|
Rhône-Alpes is the second French region as regards academic education and research, and one of the top European regions of technological innovation. Instituted in 1988 by a group of industrialists, bankers, and scientists, the Foundation Rhône-Alpes Futur aims at improving the development of the region by supporting industrial innovation, bringing together scientists and industrialists, thus contributing to the wealth creation in Rhône-Alpes. |
|
Rhône-Alpes est la seconde région française en ce qui concerne l'enseignement supérieur et la recherche, et une des premières régions européennes en innovation technologique. Instituée en 1988 par un groupe d'industriels, banquiers et scientifiques, la Fondation Rhône-Alpes Futur vise à augmenter le développement de la région en soutenant l'innovation industrielle, en réunissant les scientifiques et les industriels, contribuant ainsi à la prosperité en Rhône-Alpes. |
|
On November 21, 2002 took place at the Prefecture of Lyon the 10th edition of the symposium, which featured 48 presentations. The Information Technology Award (courtesy of France Telecom) has been attributed to Radu Mateescu for presenting the poster entitled "EVALUATOR 3.0: A Tool for Verifying Critical Systems". Radu Mateescu joined INRIA in 1994. He got an engineering degree from the Polytechnic University of Bucharest (Romania) and a PhD degree from the National Polytechnic Institute of Grenoble. He currently holds a research scientist position at INRIA Rhône-Alpes in the VASY team headed by Hubert Garavel. The works of VASY aim at improving reliability of safety-critical systems by means of formal methods. Radu Mateescu is working on value-based temporal logics, which are well-adapted formalisms for specifying properties of value-passing concurrent systems. He is the author of two model-checking tools: XTL 2.0, which has been used for verifying nine industrial safety-critical applications, and EVALUATOR 3.0 (co-authored with Mihaela Sighireanu). EVALUATOR 3.0 is a model-checking tool allowing to verify essential properties of concurrent, safety-critical systems. The verification is carried out on-the-fly, by exploring only those parts of the system's state space which are useful for deciding whether the property holds or not. Properties are described in a concise, natural way using regular alternation-free mu-calculus, a temporal logic with a rich set of operators (predicates over actions, regular expressions over sequences, modalities and fixed point operators). EVALUATOR 3.0 allows to build reusable libraries of temporal properties and generates pertinent diagnostics (portions of the state space) explaining why a safety-critical property does not hold. EVALUATOR 3.0 is part of the CADP verification toolbox and has been developed using the Open/Caesar technology. The tool was successfully used for verifying eleven industrial safety-critical systems. The most recent ones are related to products of Ericsson, The Royal Netherlands Navy, Sun MicroSystems, and Thales Nederland. Within the VASY team, EVALUATOR 3.0 is used for validating Bull's new multiprocessor architecture Fame/McKinley based upon 64-bit processors. |
Le 21 novembre 2002 a eu lieu, à la Préfecture de Lyon, la 10ème édition du symposium "Carrefours", comportant 48 présentations. Le prix "Technologies de l'information" (attribué par France Télécom) a été décerné à Radu Mateescu pour la présentation du poster intitulé "EVALUATOR 3.0: un outil pour la vérification des systèmes critiques". Radu Mateescu a rejoint l'INRIA en 1994. Il est titulaire d'un diplôme d'ingénieur de l'Université Polytechnique de Bucarest (Roumanie) et d'une thèse de doctorat de l'Institut National Polytechnique de Grenoble. Il est actuellement chargé de recherche à l'INRIA Rhône-Alpes au sein de l'équipe VASY dirigée par Hubert Garavel. Les travaux de VASY visent à améliorer la fiabilité des systèmes critiques au moyen de méthodes formelles. Radu Mateescu travaille sur les logiques temporelles étendues avec des valeurs, qui sont bien adaptées pour spécifier les propriétés des systèmes parallèles communiquant par messages. Il est auteur de deux outils de vérification: XTL 2.0, qui a été utilisé pour vérifier neuf applications industrielles critiques, et EVALUATOR 3.0 (réalisé en collaboration avec Mihaela Sighireanu). EVALUATOR 3.0 est un outil permettant de vérifier les propriétés essentielles des systèmes parallèles critiques. La vérification est effectuée à la volée, en explorant uniquement les parties de l'espace d'états du système nécessaires pour décider la validité de la propriété. Les propriétés sont décrites de façon concise et naturelle en mu-calcul régulier d'alternance 1, une logique temporelle ayant un ensemble riche d'opérateurs (prédicats sur actions, expressions régulières sur séquences, modalités et opérateurs de point fixe). EVALUATOR 3.0 permet de construire des bibliothèques réutilisables de propriétés temporelles et génère des diagnostics pertinents (portions de l'espace d'états) expliquant pourquoi une propriété critique n'est pas valide. EVALUATOR 3.0 fait partie de la boîte à outils CADP pour la vérification de systèmes critiques et a été développé au moyen de la technologie Open/Caesar. L'outil a été utilisé avec succès pour vérifier onze applications industrielles critiques. Les plus récentes portent sur des produits d'Ericsson, de la Marine Royale des Pays-Bas, de Sun MicroSystems et Thalès Pays-Bas. Au sein de l'équipe VASY, EVALUATOR 3.0 est utilisé pour valider la nouvelle architecture multiprocesseurs Fame/McKinley de Bull à base de processeurs 64 bits. |
Back to the VASY Home Page
