page d'accueil   sommaire   faculté  

Méthodes formelles et vérification [Verification and formal methods] (Verif)
Faculté des Sciences / faculty of Sciences - Informatique (unité ULB512)

Le service méthodes formelles et vérification consacre ses efforts de recherche et d'enseignement aux méthodes rigoureuses et automatiques qui permettent de concevoir des systèmes informatiques fiables. Ces méthodes trouvent des applications naturelles dans la conception de systèmes informatiques critiques, comme les systèmes de contrôle embarqués dans les moyens de transport (métros, avions, voiture), les systèmes de contrôle de production (dans un cadre industriel), etc. [The research and teaching activities of the ''formal methods and verification group'' deal with rigourous methods that allow to design reliable computer systems. These methods are usually applied in the context of critical systems, such as embedded systems in transportation (trains, planes, cars), plants control systems, and so forth. ]



coordonnées / contact details


Méthodes formelles et vérification [Verification and formal methods]
tel +32-2-650.56.14, fax +32-2-650.56.09, Thierry.Massart@ulb.ac.be
http://www.ulb.ac.be/di/verif
Campus de la Plaine, Campus de la Plaine, Bâtiment NO, 8è étage
CP212, boulevard du Triomphe, 1050 Bruxelles

Pour en savoir plus, consultez le site web de l'unité.



responsables / head


Prof. Thierry MASSART Jean-François RASKIN


composition / members


Emmanuel FILIOT Pierre GANTY Gilles GEERAERTS Christian HERNALSTEEN Gabriel KALYON SHIRMOHAMMADI MAHSA Frédéric SERVAIS Laurent VAN BEGIN


projets / projects


ARTIST 2
Artist 2 est un réseau d'excellence du 6ème programme cadre de l'Union Européenne sur le développement fiable de systèmes embarqués. Nous participons plus particulièrement au cluster ''Test and Verification of Embedded Systems'' du NoE. Voir http://www.artist-embedded.org/artist/ [Artist 2 is an excellence network of the 6th framework programme of the European Union dedicated to the reliable development of embedded and embarked systems. We take part more specifically in the cluster ''Test and Verification of Embedded Systems'' of the NoE. See http://www.artist-embedded.org/artist/]

Centre Fédéré en Vérification [Federated Center in Verification]
Le Centre Fédéré en Vérification est un groupe de travail qui regroupe les équipes de recherche actives en vérification assistée par ordinateur en Communauté Wallonie-Bruxelles de Belgique. Il existe depuis 1999 et est financé par le Fonds National de la Recherche Scientifique Belge (convention FRFC n° 2.4530.02) depuis 2002. Le groupe de travail organise des séminaires et donne un cadre officiel aux collaborations de recherche entre les différentes équipes qui le composent. Voir http://www.ulb.ac.be/di/ssd/cfv/ [The CVF is a working group gathering the various teams working on computer aided verification in the Communauté Wallonie-Bruxelles in Belgium. Funded by the FNRS (FRFC 2.4530.02), the group organizes seminars and offer a common and collaborative framework for the various groups in it. See http://www.ulb.ac.be/di/ssd/cfv/]

Superviseurs corrects, efficaces et robustes [Correct, efficient and robust controllers]
La mise au point d'un environnement de conception de logiciels de superviseurs et de contrôleurs industriels distribués conduit à de nombreux problèmes intéressants, en particulier la définition d'outils de distribution automatique de code et de modules de validation de ces logiciels pour augmenter leur fiabilité. [The elaboration of a framework for the development of distributed industrial supervisors and controllers leads to interesting problems, in particular to tools for the automatic distribution of codes and validation modules to improve their robustness.]

Quasimodo: Propriétés quantitatives des systèmes dans la conception de systèmes embarqués à partir de modèles [Quasimodo: Quantitative System Properties in Model-Driven-Design of Embedded Systems]
Le but de Quasimodo est le développement de nouvelles techniques et de nouveaux outils pour la conception, l'analyse, le test et la génération de code à base de modèles dans le cadre des systèmes embarqués pour lesquels il est important de pouvoir assurer des bornes sur la consommation des ressources. Voir: http://www.quasimodo.aau.dk/ [The main goal of Quasimodo is to develop new techniques and tools for model-driven design, analysis, testing and code-generation for advanced embedded systems where ensuring quantitative bounds on resource consumption is a central problem. See: http://www.quasimodo.aau.dk/]

GASICS: théorie des jeux pour l'analyse et la synthèse de systèmes informatiques interactifs [GASICS: Games for Analysis and Synthesis of Interactive Computational Systems]
Le projet GASICS étudie les formalisations à l'aide de la théorie des jeux des systèmes informatiques interactifs, et développe des algorithmes pour les analyser et les synthétiser. Le but de projet est d'étendre la théorie classique des jeux joués sur des graphes à deux joueurs et à somme nulle, à des cas à plusieurs joueurs et à somme non-nulle. Le projet vise également à montrer l'applicabilité de ces nouvelles théories à l'analyse et à la synthèse de systèmes informatiques interactifs. Voir: http://www.ulb.ac.be/di/gasics/ [The gasics project studies game theoretic formalizations of interactive computational systems and algorithms for their analysis and synthesis. Our aim is to extend the existing notions of games played on graphs introduced by computer scientists. Currently, most of the games played on graphs are of the sort ''two players-zero sum'', we aim to extend them to ''multiple players non-zero sum'', and show the applicability of the new theory to the analysis and synthesis of interactive computational systems. See: http://www.ulb.ac.be/di/gasics/]

MOVES: modélisation, vérification et évolution de logiciel [MOVES: Fundamental Issues in Modelling, Verification and Evolution of Software]
Voir http://moves.vub.ac.be/ [See http://moves.vub.ac.be/]



publications





theses


Nicolas Maquet (2011), New Algorithms and Data Structures for the Emptiness Problem of Alternating Automata, Dir. Prof. J-F Raskin, Dept. Informatique, Fac des Sciences, ULB, 2011

Kalyon, Gabriel. (2010), ''Supervisory Control Of Infinite State Systems Under Partial Observation'', Dir. Prof. Thierry Massart, Département d'Informatique, ULB, Bruxelles., 2010

Gilles Geeraerts (2007), Coverability and Expressiveness properties of well-structured transition systems, Dir. Prof. J-F Raskin, Dept. Informatique, Fac des Sciences, ULB, 2007

Pierre Ganty (2007), The Fixpoint Checking Problem: an Abstraction Refinement Perspective, Dir. Prof. J-F Raskin, Dept. Informatique, Fac des Sciences, ULB, 2007

Doyen, L. (2006), ''Algorithmic Analysis of Complex Semantics for Timed and Hybrid Automata'', Dir. Prof. J-F. Raskin, Département d'Informatique, ULB, Bruxelles., 2006

De Wulf, M. (2006), ''From timed models to timed implementations'', Dir. Prof. J-F. Raskin, Département d'Informatique, ULB, Bruxeles., 2006

De Wachter, B. (2005), ''dSL, a language and environment for the specification of distributed industrial controllers'', Dir. Prof. T.Massart, Département d'Informatique, ULB, Bruxelles., 2005

Van Begin, L. (2003), ''Efficient Verification of Counting Abstractions for Parametric systems'', Dir. Prof. J-F. Raskin, Département d'Informatique, ULB, Bruxelles., 2003

Kremer, S. (2003), ''Formal Analysis of Optimistic Fair Exchange Protocols'', Dir. Profs. J-F. Raskin et Y. Roggeman, Département d'Informatique, ULB, Bruxelles., 2003

Raskin, J-F. (1999), ''Logics, Automata and Classical Theories for Deciding Real Time'', Dir. P-Y. Schobbens, Pôle sémantique, logique et calcul, FUNDP, Namur., 1999

Hernalsteen, C. (1998), ''Specification, Validation and Verification of Real-Time Systems in ET-LOTOS'', Dir. Prof. T. Massart, Département d'Informatique, ULB, Bruxelles., 1998

Massart, T. (1990) ''A basic agent calculus and bisimulation laws for the design of systems'', Dir. Prof. R. Devillers, Laboratoire d'Informatique, ULB, Bruxelles, 1990



collaborations


Hubert Garavel :, INRIA Rhône-Alpes, (VASY team), Montbonnot Saint-Martin,, France

Prof. Michael Leuschel :, Heinrich-Heine-Universität, (Institut für Informatik, Softwaretechnik und Programmiersprachen), Düsseldorf,, ALLEMAGNE (REP.FED.)

Thierry Jéron :, IRISA-INRIA, (VERTECS project), Rennes,, France

Prof. Emmanuel Jeannot :, INRIA Lorraine, (Loria, équipe Algorille), Nancy,, France

Prof. Thomas Henzinger :, EPFL, (Computer and Communication Sciences: Models and Theory of Computation), Lausanne,, Suisse

Prof. Giorgio Delzanno :, University of Genova, (DISI), Genova,, Italie

Prof. Pierre-Yves Schobbens :, FUNDP, (Institut d'Informatique), Namur,, Belgique

Prof. Véronique Bruyère :, Université de Mons-Hainaut, (Institut d'Informatique), Mons, Belgique

Dr. Franck Cassez :, Ecole Centrale de Nantes, (IRCyN), Nantes,, France

Prof. Alain Finkel :, ENS Cachan, (LSV), Cachan,, France

Prof. Yassine Lakhnech :, Université Joseph Fourier, (VERIMAG), Gieres (Grenoble),, France

Dr. Bruno Dutertre :, Stanford Research Institute, (Computer Science Laboratory), Menlo Park (Stanford),, Etats-Unis (USA)

Prof. Thomas Brihaye, Université de Mons, Mathématiques Effectives, Mons, Belgique

Prof. Joël Ouaknine, Oxford University, Computing Laboratory, Oxford, Grande-Bretagne

Prof. James Worrell, Oxford University, Computing Laboratory, Oxford, Grande-Bretagne

Prof. Pierre Ganty, Fundación IMDEA Software, Facultad de Informática, Madrid, Espagne

Prof. Marcin Jurdzinski, University of Warwick, Computer Science Department, Warwick, Grande-Bretagne

Prof. Patrick Cousot, ENS Paris, Paris, France

Dr. Laurent Doyen, ENS Cachan, Laboratoire Spécification et Vérification, Cachan, France

Prof. Krishnendu Chatterjee, Institute of Science and Technology Austria, Vienne, Autriche

Prof. Pierre-Alain Reynier, Université de Provence, Laboratoire d'Informatique Fondamentale, Marseille, France

Prof. Kim G. Larsen, Aalborg University, Department of Computer Science, Aalborg, Danemark

Hervé Marchand, INRIA Bretagne, Vertecs, Rennes, France



prix / awards


Prix F.R.S/FNRS ''IBM Belgium'' 2000 pour une thèse de doctorat - Laurent VAN BEGIN

Prix F.R.S/FNRS ''IBM Belgium'' 2007 pour une thèse de doctorat - Gilles GEERAERTS

Prix F.R.S/FNRS ''IBM Belgium'' 2000 pour un mémoire de fin d'étude - Laurent VAN BEGIN



savoir-faire/équipements / know-how, equipment


Expertise dans la conception de systèmes informatique fiables



mots clés pour non-spécialistes / keywords for non-specialists


systèmes critiques systèmes embarqués vérification assistée par ordinateur vérification de systèmes informatiques


disciplines et mots clés / disciplines and keywords


Analyse de systèmes informatiques Informatique appliquée logiciel Informatique générale Informatique mathématique

consommation de resources contrôle distribué distribution de code evolution logicielle génération de code logiciel robustesse synthèse de logiciel systèmes embarqués systèmes informatiques interactifs temps-réel théorie des jeux verification assistée par ordinateur vérification de logiciels verification logicielle


codes technologiques DGTRE


Informatique, théorie des systèmes Sciences de l'ordinateur, analyse numérique, systèmes, contrôle