VERIMAG/RSD team is led by Saddek Bensalem.
Rationale and Objectives
Our research agenda focuses on rigorous system design as a coherent and accountable process aimed at building cost-effectively systems of guaranteed quality. The aim is to provide the theoretical underpinnings, methods and tools for moving from empirical approaches to a well-founded discipline. We study system design as a formal systematic process supported by a methodology. In our methodology we clearly identify segments of the design process that can be supported by tools to automate tedious and error-prone tasks. We also clearly distinguish points where human intervention and ingenuity are needed to resolve design choices through requirements analysis and confrontation with experimental results. Identifying adequate design parameters and channeling the designers’ creativity are essential for achieving design goals.
What is Rigorous System Design?
A rigorous system design flow is a formal accountable and iterative process for deriving trustworthy and optimized implementations from application software and models of its execution platform and its external environment. Rigorous system design is a formally defined process decomposed into steps. It is also model-based: successive system descriptions are obtained by application of correct-by-construction source-to-source of a single expressive model rooted in well-defined semantics. An additional demand is accountability that is the possibility to explain which among the requirements is satisfied and which may not be satisfied.
Work Directions – The BIP Framework
The BIP (Behavior / Interaction / Priority) framework is intended to design and analysis of complex, heterogeneous embedded applications. BIP is a highly expressive, component-based framework with rigorous semantics. It allows the construction of complex, hierarchically structured models from atomic components.
The pursued research directions are the following:
- Study notions of embedding of domain specific languages into BIP.
- Study of scalable verification techniques, including compositional verification techniques for deadlock-freedom and invariant properties.
- Study of correct-by-construction implementation techniques, targeting distributed real-time systems and mixed-criticality systems.
- Modeling and analysis of mixed software/hardware system models.
