Post-doctorate proposal - INRIA project-team TEA, Rennes
Post-doctorate proposal - INRIA project-team TEA, Rennes
Synthesis of multi-periodic systems from architecture modelling standards
INTRODUCTION
An architecture model is a system design artifact at the crossing of all
constituents of a cyber-physical system, its software (programs,
controllers, drivers, operating system), its hardware (sensors, actuators,
bus, processors, memory), and its d/c interfaces with the physical
environment. Time plays a prominent role in the design and integration of
these constituents. It is discrete, event-driven, in software design;
discrete, time-triggered, periodic, multi-periodic in hardware design; and
continuous in physics. It becomes central from the architect's
standpoint, whose task is to mitigate heterogeneous timing models to build
a reliable system, e.g., to schedule the execution of software (logical
time, causality) on hardware (periodic, multi-periodic) by building
abstractions (e.g. WCET approximation, end-to-end latency).
PROJECT
In this project, we are considering embedded architecture design
standards, such as the SAE AADL and SysML. In the spirit of MARTE's CCSL
(clock constraint specification language), we aim at the definition and
implementation of formal semantics to represent timed behaviors and
properties of modeling artifacts in these standards. Starting from an
existing implementation of these principles, which uses Eclipse Pop's
polychronous model of computation to simulate and generate code from AADL
behavior specifications, we wish to address the model-based synthesis of
real-time, multi-periodic, systems from specifications in, e.g., AADL,
SysML's PSSMs, CCSL, exhibiting multiple, related, clock domains, and by
using an existing real-time scheduler synthesis tool, ADFG.
OBJECTIVE
The aim of the post-doctorate is to participate in every aspect of the
project, by contributing to the formalization of time domains and time
relations in the proposed semantic framework, to the specification of the
standards formal semantics, to normative documents, and to the
implementation of our reference prototype.
REQUIREMENTS
Candidates should have a Ph.D. degree in computer science, combine solid
theoretical background in the theory of concurrency, language design,
program analysis, as well as prototype software development skills.
Knowledge and experience with synchronous languages and/or model-driven
engineering and/or the AADL, MARTE/CCSL, PSL, SysML standards will be
favored, as well as experience with open-source, model-driven, reactive
and synchronous environments such as Pop, Osate, Papyrus, Kieler, or
Ptolemy. The work will be conducted with INRIA project-team TEA in Rennes,
Brittany, France. The initial duration of the post-doctorate is adjustable
from 12 to 18 months, possibly renewable. The position is available
immediately.
REFERENCES
"Formal semantics of behavior specifications in the architecture analysis
design language". L. Besnard, T. Gautier, P. Le Guernic, C. Guy, J.-P.
Talpin, B. Larson, E. Borde. In High-Level Design Verification and Test
(HLDVT'16). IEEE, 2016. Also available as Inria technical report n. 8950.
"Timed behavioural modelling and affine scheduling of embedded software
architectures in the AADL using Polychrony". L. Besnard, A. Bouakaz, T.
Gautier, P. Le Guernic, Y. Ma, J.-P. Talpin, H. Yu. In Science of Computer
Programming (SCP). Elsevier, 2014.
"From AADL to timed abstract state machine: a certified model
transformation". Z. Yang, K. Hu, D. Ma, J.-P. Bodeveix, L. Pi, J.-P.
Talpin. In Journal of System and Software (JSS). Elsevier, 2014.
"Polychronous modeling, analysis, verification and simulation for timed
software architectures". H. Yu, Y. Ma, T. Gautier, L. Besnard, P. Le
Guernic, J.-P. Talpin. In Journal of Systems Architecture (JSA). Elsevier,
2013.