Logically timed specifications in the AADL : a synchronous model of computation and communication (recommendations to the SAE committee on AADL)

The purpose of this document is to provide an analysis of the SAE standard AADL (AS5506) and submit recommendations for equipping it with a synchronous model of computation and communication (MoCC). Our goal is to provide a framework that best fits the semantic and expressive capability of the AADL, and is designed in a way that requires as few conceptual, semantic, or syntactic extensions as possible, on either the standard or its existing annexes. Our approach consists of the definition of an algebraic framework in which time is formally defined from implicit or specified AADL concepts, such as events. Starting from these concepts, that constitute the synchronous core of the AADL, we define a formal design methodology to use the AADL in a way that supports formal analysis, verification and synthesis of timed properties. By putting forward synchrony and timing, we intend to define time starting from software and hardware events that incur synchronisation in an architecture specification. Synchronisation indeed is the fundamental artefact from which time can be sensed, in either software or hardware. Synchrony relates to that fundamental concept as a model of computation and communication, applicable to both software and hardware design. It puts emphasis on logical time, abstracted through synchronisation points, in order to break down computations into zero-time reactions and regard communications as instantaneous. While abstracting real time, synchronous logical time provides an algebraic framework in which both event-driven and time-triggered execution policies can be specified. Bridging the gap between system-level, logical, synchronous specifications and time-triggered, distributed, and dynamically scheduled real-time applications necessitates a refinement-based design methodology, which we additionally intend to outline, to support the applicability of the proposed concepts in system design. To support the formal presentation of our MoCC, we define a algebra of automata consisting of transition systems and logical timing constraints. We consider the behaviour annex (BA) as the mean to implement this model, together with the constraint annex (CA), as a mean to represent abstractions of behaviour annexes using clock constraints and regular expressions.L'architecture logiciel d'un système embarqué est un artefact de conception de constituants hétérogènes au croisement de plusieurs points de vue: logiciel, matériel, physique. Le temps à une nature différente quand il est observé de ces points de vue différents : il est discret et évènementiel vu du logiciel, discret et périodique vu du matériel, et continu en physique. Il n'est pas surprenant que ce soit une notion commune à l'architecte d'un système, étant donné sa criticité, sa diversité, la difficulté de le maitriser. Pour compliquer les choses un peu plus, les formalismes de spécification et de programmation de haut-niveau utilisés pour spécifier ces systèmes altèrent significativement cette perception du temps. Dans un modèle physique, on simule le temps par des équations différentielles dont la résolution est discrète. Dans un modèle matériel, on représente les circuits par différents niveaux d'abstractions pour faire face à leur complexité: registre, transaction, système. Dans un modèle logiciel, on abstrait le temps par un modèle conceptuel de la concurrence, pas exemple synchrone. Délivrer un cadre mathématique, des outils de vérification et de synthèse, pour analyser, composer, orchestrer ces modèles serait d'une valeur inestimable pour l'architecte d'un système. L'architecte travaille en effet d'un point de vue ou' toutes les composantes d'un système: logiciel, intergiciel, matériel, environnement; doivent être analysés, profilés, évalués, composés, simulés et validés. L'objectif de ce document est de proposer un cadre méthodologique formel pour conduire le travail de l'architecte: l'exploration d'architecture et le prototypage virtuel de systèmes embarqués. Pour définir cette méthodologies, nous nous appuyons sur le standard AADL (architecture analysis description language) du consortium SAE, auquel nous recommandons la définition d'une annexe temporelle au standard