LYON, France, November 21, 2002 - Dr. Radu Mateescu, research scientist at INRIA Rhône-Alpes in the VASY team, has won the Information Technology Award attributed during the 10th edition of the yearly symposium organized by the Foundation Rhône-Alpes Futur.

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.


IT Award Winner - Dr. Radu Mateescu
LYON, France, 21 novembre 2002 - Dr. Radu Mateescu, chargé de recherche à l'INRIA Rhône-Alpes dans l'équipe VASY, a remporté le Prix "Technologies de l'information" décerné lors de la 10ème édition du symposium organisé par la Fondation Rhône-Alpes Futur.

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.

Since 1992, the Foundation organizes every year a symposium that tightens the collaboration between researchers, industrialists, and public institutions. This symposium features presentations of results belonging to seven strategic research areas: bio-industries, economy and society, modelisation and simulation, information technology, enterprise creation, environment, mechanics and nano-technologies. For each research area, an award is attributed to the scientific achievements having the most promising potential for industrial transfer.

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.
Depuis 1992, la Fondation organise chaque année les "Carrefours", un symposium qui renforce la collaboration entre chercheurs, industriels et institutions publiques. Cet événement comporte des présentations de résultats dans sept domaines de recherche stratégiques : bio-industries, économie et société, modélisation et simulation, technologies de l'information, création d'entreprises, environnement, mécanique et nano-technologies. Pour chaque domaine de recherche, un prix est décerné aux contributions scientifiques ayant le potentiel le plus élevé pour le transfert industriel.

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.

Additional information

Region Rhône-Alpes

Foundation Rhône-Alpes Futur

"Carrefours" symposia

France Telecom

INRIA and INRIA Rhône-Alpes

VASY research project

Radu Mateescu's Home Page

Mihaela Sighireanu's Home Page

Radu Mateescu's poster

About CADP and Open/Caesar

About EVALUATOR 3.0

Informations complémentaires

Région Rhône-Alpes

Fondation Rhône-Alpes Futur

Symposium "Carrefours"

France Télécom

INRIA et INRIA Rhône-Alpes

Projet VASY

Page personnelle de Radu Mateescu

Page personnelle de Mihaela Sighireanu

Poster de Radu Mateescu

A propos de CADP et Open/Caesar

A propos d'EVALUATOR 3.0



Version 1.15 - Date 2015/09/18 16:02:58
Back to the VASY Home Page