Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony

• Virtual prototyping of AADL architectures in a synchronous model of computation.
• Synchronous framework for modelling and verification of AADL specifications.
• Definition, development and case-study validation of an AADL simulation framework.
• Efficient affine abstraction and schedule synthesis from AADL timing constraints.

High-level modelling languages and standards, such as Simulink, UML, SysML, MARTE and AADL (Architecture Analysis & Design Language), meet increasing adoption in the design of embedded systems in order to carry out system-level analysis, verification and validation (V&V) and architecture exploration, as early as possible. These analysis, V&V, architecture exploration techniques rely on mathematical foundations and formal methods in order to avoid semantics ambiguities in the design of safety-critical systems.In order to support integration validation, it is necessary to define a formal framework of virtual prototyping to integrate, verify, exercise and analyse the application code generated by modelling tools as early as possible and virtually integrate it with simulators of third-party middleware and hardware. Such a virtual prototyping platform makes it possible to validate the expected behaviour of the final application software and check that the resulting system indeed meets the specified performance requirements before the actual hardware even actually exists.In this paper, we present the definition, development and case-study validation of such a comprehensive framework, based on the synchronous paradigm and the polychronous model of computation and communication of its supportive open-source toolset: Polychrony. A longer-term aim of our work is to equip the AADL standard with an architecture-centric framework allowing for synchronous modelling, verification and synthesis of embedded software.