Toward Polychronous Analysis and Validation for Timed Software Architectures in AADL

International audienceHigh-level architecture modeling languages, such as Architecture Analysis & Design Language (AADL), are gradually adopted in the design of embedded systems so that design choice verification, architecture exploration, and system property check- ing are carried out as early as possible. This paper presents our recent contributions to cope with clock-based timing analysis and validation of software architectures specified in AADL. In order to avoid semantics ambiguities of AADL, we mainly consider the AADL features related to real-time and logical time properties. We endue them with a semantics in the polychronous model of computation; this semantics is quickly reviewed. The semantics enables timing analysis, formal verification and simulation. In addition, thread-level scheduling, based on affine clock relations is also briefly presented here. A tutorial avionic case study is finally adopted to illustrate our overall contribution