We tackle several phases in the design of correct-by-construction real-time embedded systems:
- High-level modeling and formal semantics
- Links between theoretical and engineering models
- Functional and logical time correctness
- Sound transformation and analysis technique
- Mapping of concurrent applications onto parallel and/or multicore architectures
We get an initial focus from concurrency theory models, such as data-flow process networks and synchronous reactive languages. We also consider transformations from nested loop (sequential imperative) code into an homogeneous framework (as process networks).
In all these cases a first-level semantics (self-timed) can be refined into a second-level semantics (scheduled), asserting precisely the temporal activation conditions for processing operations (computations or communications). These activation patterns are called Logical Clocks, and as schedule patterns they become explicit design ingredients. Precise schedules can be computed to optimize various factors (Throughput, buffer queue sizes, power consumption,...).
The AAA (Algorithm/Architecture Adequation, or also Application/Architecture Allocation) adds one more dimension, demanding that the scheduling is combined with a mapping relation that asociates the computations and communications to processing and interconnect resources on a described architecture model (usually distributed or multicore). Further optimization criteria may take place here. Similar role can be played by user or system requirements instead of an architecture model.
We attempted to generalize all this by defining a generic Logical Time approach, based on logical clocks and constraints between them. This effort was carried all the way to its official inclusion in the OMG UML MARTE profile (Modeling and Analysis of Real-Time Embedded systems), together with provision for non-functional property assertions which may guide the desired optimizations and constraint solvers.
Most of our practical work thus consists in defining efficient operational semantics based on scheduling techniques and results, as well as model-based optimizations of systems. Conflict-free behavioral independence of system parts, known as endochrony in the synchronous community, is an instance of such optimization feature.
Model-based editors and transformations supporting the approach in a visually appealing way are also an issue for us.
We illustrate our results in connection with domain-specific formalisms such as AADL for avionics; EAST-ADL for AutoSar automotive; and with greater emphasis for SystemC/IP-XACT for component-based System-on-Chip design.
A more detailed description of Aoste recent research topics can be found in our INRIA Activity Reports: