CONVECS Research team
Construction of verified concurrent systems
- Leader : Radu Mateescu
- Type : Project team
- Research center(s) : Grenoble
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Embedded and Real-time Systems
- Partner(s) : Institut polytechnique de Grenoble,Université Joseph Fourier (Grenoble)
- Collaborator(s) : Laboratoire d'Informatique de Grenoble (LIG) (UMR5217)
Team presentationCONVECS is a research team working on the formal modeling and verification of asynchronous concurrent systems, which are instantiated in various domains (communication protocols, distributed algorithms, cloud computing, Globally Asynchronous Locally Synchronous systems - GALS, etc.). To this aim, CONVECS proposes new formal languages for specifying the behaviour and the properties of concurrent systems, and devises efficient verification algorithms and tools running on sequential machines and distributed infrastructures.
Research themesAsynchronous concurrency is becoming ubiquitous, from the micro scale of embedded systems and multi-core processors to the macro scale of grids and cloud computing. In the race for improved performance and lower power consumption, computer manufacturers are moving towards asynchrony, in which several entities operate concurrently at different speeds, communicate and synchronize. The price to pay for enhanced performance is an increased design complexity, which can only be addressed by formal verification.
To improve the state-of-the-art in the design and analysis of concurrent asynchronous systems, CONVECS follows a research programme of five interrelated scientific topics:
- Going from high-level formal languages to concurrent implementations.
- Parallel and distributed verification algorithms.
- Handling of timed, probabilistic, and stochastic aspects.
- Component-based architectures for on-the-fly verification.
- Real-world applications and case-studies.
International and industrial relationsThe CONVECS team is involved in several international working groups in the domain of formal methods and verification:
- FMICS ERCIM Working Group on Formal Methods for Industrial Critical Systems
- IFIP Working Group 1.8 on Concurrency Theory
- AVACS consortium on Automatic Verification and Analysis of Complex Systems
(involvement of Hubert Garavel in cooperation with Saarland University)
Research teams of the same theme :
- AOSTE2 - Models and methods of analysis and optimization for systems with real-time and embedded contraints
- HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
- KAIROS - Logical Time for Formal Embedded System Design
- PARKAS - Parallélisme de Kahn Synchrone
- SPADES - Sound Programming of Adaptive Dependable Embedded Systems
- TEA - Time, Events and Architectures