Joseph Sifakis
Tel: (+33) 457 42 22 44

R&D Projects
Joseph Sifakis
  • SPEEDS IST Project (2006-2009): «Speculative and Exploratory Design in Systems Engineering », in collaboration with Airbus, Daimler, IAI, INRIA, OFFIS, PARADES.
  • OpenEmbedd RNTL platform (2005-2008):
  • Omega IST projet (2002-2004) «Correct Development of Real-Time Embedded Systems » in collaboration with France Telecom and EADS Space.
  • Expresso RNTL projet (2001-2003) « Real-time JAVA for embedded systems» in collaboration with SILICOMP, Aonix and IRISA.
  • Taxys RNRT projet (1999-2001) : Analysis of synchronous embedded software for cellular phones, in collaboration with Alcatel Business Systems et France Télécom.
  • Proust RNRT project (1998-2000): Definition of a timed extension for the SDL international standard of ITU.
  • DDV project (1993-1995) : Evaluation of formal techniques on a fault-tolerant architecture, ESA/ESTEC, in collaboration with Matra-Marconi-Space and Dornier.
  • VIRES project (1996-1999): Verifying Industrial Reactive Systems, European Long Term Research Project.
  • REACT project (1993-95): Building Correct Reactive Systems, European Long Term Research Project.
  • Spec project (1990-92): Formal Methods and Tools for the Development of Distributed and Real-Time Systems, European Basic Research Project.
  • TGV project (1994-95).: Joint Verilog-Verimag-Irisa project for the development of a test case generation tool from test purposes and SDL models of communication protocols.
  • Caesar project and the CADP toolset (1989-92) : Development of a compiler/model checker for the LOTOS language by H. Garavel. The CADP integrates Caesar and a set of static analysis and verification tools.
  • Vesar project (1988-90): Development of an environment integrating Xesar and the test case generator VEDA of France Telecom, in collaboration with Verilog SA.
  • Xesar project (1985-87): Development under France Telecom contract of a model-checker for the Estelle ISO standard for communication protocols. Xesar has been succesfully used in the Esprit Delta-4 project for the validation of a fault-tolerant token-ri,ng protiocol in collaboration with Bull and Laas (1988-90).