- ALIDECS / ACI “Sécurité & Informatique” French Programme, 2004-2007
- OpenES 2013-2016
- CIFRE STMicroeletronics 2018-2021
- Tayeb Bouhadiba, PhD 2006-2010
- Giovanni Funchal, PhD 2007-2011
- Yuliia Romenska , PhD 2013-2017
- Vincent Morice, PhD 2018-2021
In the context of the OpenES project, we designed a very general and high-level notion of a component for hardware/software systems, for which functional properties can be specified in a contract-like formalism. Contrary to a lot of component models at this level of abstraction, our framework is executable. A non-deterministic component can be “executed” if, given inputs, we are able to generate random outputs such that the non-deterministic contract that links inputs and outputs is satisfied. This method relies on constraint solvers. We defined a formalism and execution engine compatible with existing SystemC/TLM components.
We are now starting to work on the idea of a “quality of use” contract for a HW/SW component. In the execution of a system made of several components (some of them given in full details, some of them described by their contracts only), we will define warnings, able to identify situations in which, for instance, a piece of software makes a non-optimal use of a HW component (e.g., if it offers a DMA-like memory transfer, but the SW does not use it).
The work on components is inspired by the various notions of components we’ve worked with in the following domains:
- Embedded control, especially with synchronous languages; case-studies in SCADE (the commercial programming environment based on Lustre); previous work on contracts for reactive systems (see Lionel Morel, PhD 2001-2005).
- Transaction-Level Modeling (TLM) of systems-on-a-chip
- Virtual Prototyping of various embedded and communicating systems (e.g., sensor networks)
- Efficient Monitoring of Loose-Ordering Properties for SystemC/TLM (DATE’16)
- Specification and Validation of Embedded Systems: A Case Study of a Fault-Tolerant Data Acquisition System with Lustre Programming environment
- Formal and Executable Contracts for Transaction-Level Modeling in SystemC
- Contract-Based Coordination of Hardware Components for the Development of Embedded Software
- Defining and translating a “safe” subset of Simulink/Stateflow into Lustre
- Logical-Time Contracts for the Development of Reactive Embedded Software
- Arrays and Contracts for the Specification and Analysis of Regular Systems
- 42: Programmable Models of Computation for a Component-Based Approach to Heterogeneous Embedded Systems