Zhibin Yang
email: zhibin.yang@irit.fr

Kai Hu
email: hukai@buaa.edu.cn

Dianfu Ma
email: dfma@buaa.edu.cn

Jean-Paul Bodeveix
email: bodeveix@irit.fr

Lei Pi
email: lei.pi@intecs.it

Jean-Pierre Talpin

From AADL to Timed Abstract State Machines: A verified model transformation

Architecture Analysis and Design Language (AADL) is an architecture description language standard for embedded real-time systems widely used in the avionics and aerospace industry to model safety-critical applications. To verify and analyze the AADL models, model transformation technologies are often used to automatically extract a formal specification suitable for analysis and verification. In this process, it remains a challenge to prove that the model transformation preserves the semantics of the initial AADL model or, at least, some of the specific properties or requirements it needs to satisfy. This paper presents a machine checked semantics-preserving transformation of a subset of AADL (including periodic threads, data port communications, mode changes, and the AADL behavior annex) into Timed Abstract State Machines (TASM). The AADL standard itself lacks at present a formal semantics to make this translation validation possible. Our contribution is to bridge this gap by providing two formal semantics for the subset of AADL. The execution semantics provided by the AADL standard is formalized as Timed Transition Systems (TTS). This formalization gives a reference expression of AADL semantics which can be compared with the TASM-based translation (for verification purpose). Finally, the verified transformation is mechanized in the theorem prover Coq.

Introduction

Embedded real-time systems, such as those for avionics and aerospace platforms, represent one of the most safety-critical categories of system. Their system behaviors do not only rely on the software/hardware architecture, but also rely on the runtime environment, such as scheduling, communication and reconfiguration. Moreover, they are more and more complex, so reducing the development cost and time is an important element of design in these systems [START_REF] Van Vliet | Software Engineering-Principles and Practice[END_REF].

The Architecture Analysis and Design Language (AADL) [START_REF] Sae | AS5506A: Architecture Analysis and Design Language[END_REF]) is an SAE International (formerly known as the Society of Automotive Engineers) standard (SAE AS5506). AADL employs formal modeling concepts for the description of software/hardware architecture and runtime environment in terms of distinct components and their interactions, and it is especially effective for model-driven design of complex embedded real-time systems [START_REF] Walker | Automatic optimisation of system architectures using EAST-ADL[END_REF].

A safety-critical system is often required to pass stringent qualification and certification processes (for example DO-178C) before its deployment. When described using an AADL model, such a system specification is often transformed to another formal model for verification and analysis. Examples of such transformations are numerous: translations to Behavior Interaction Priority (BIP) [START_REF] Chkouri | Translating AADL into BIP -application to the verification of real-time systems[END_REF], to TLA+ [START_REF] Rolland | Modes in asynchronous systems[END_REF], to real-time process algebra ACSR [START_REF] Sokolsky | Schedulability analysis of AADL models[END_REF], to IF [START_REF] Abdoul | AADL execution semantics transformation for formal verification[END_REF], to Fiacre [START_REF] Berthomieu | Formal verification of AADL specifications in the topcased environment[END_REF], to Real-Time Maude (Ölveczky et al., 2010), to Lustre [START_REF] Jahier | Virtual execution of AADL models via a translation into synchronous programs[END_REF], to Polychrony [START_REF] Ma | Distributed simulation of AADL specifications in a polychronous model of computation[END_REF], etc. The goal of such a translation is to reuse existing verification and analysis tools and their formal model of computation and communication for the purpose of validating the AADL models. One challenge, however, is the problem of proving that the translation itself preserves the intended semantics of the AADL model in the first place or, at least, some of the specific properties or requirements it needs to satisfy [START_REF] Cabot | Verification and validation of declarative model-to-model transformations through invariants[END_REF][START_REF] Lano | Constraint-based specification of model transformations[END_REF][START_REF] Giese | Towards verified model transformations[END_REF][START_REF] Narayanan | Towards verifying model transformations[END_REF][START_REF] Narayanan | Verification of Model Transformations[END_REF][START_REF] Guerra | Automated verification of model transformations based on visual contracts[END_REF][START_REF] Kessentini | Example-based model-transformation testing[END_REF][START_REF] Mottu | Model transformation testing: oracle issue[END_REF][START_REF] Xiong | Towards automatic model synchronization from model transformations[END_REF].

This paper presents a machine checked semantics-preserving transformation of a subset of AADL into Timed Abstract State Machines (TASM) [START_REF] Ouimet | A Formal Framework for Specification-Based Embedded Real-Time System Engineering[END_REF]Lundqvist, 2006, 2008). TASM is an extension of the Abstract State Machine (ASM) formalism [START_REF] Börger | The origins and the development of the ASM method for high level system design and analysis[END_REF], which supports the specification of timing and resource consumption as well as behavior and communication. Compared with the existing approaches such as translations to BIP, TLA+, ACSR, IF, Fiacre, Real-Time Maude, Lustre, etc., we consider some resource information in the transformation. Furthermore, a formal proof of the semantics preservation of the transformation has not been considered by them. In this work, the theorem prover Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development (CoqArt: The Calculus of Inductive Constructions)[END_REF]) is used to prove the methodology, i.e. the correctness of the translation.

Following the global idea, we would like to provide a verified tool chain for the end users (as shown in Fig. 1). The first version of the model transformation tool prototype AADL2TASM has been implemented in ATL (ATLAS Transformation Language) [START_REF] Jouault | ATL: a QVT-like transformation language[END_REF] directly. AADL2TASM is a plug-in of the AADL modeling environment OSATE [START_REF] Cmu | An Extensible Open Source AADL Tool Environment[END_REF], which supports model checking using UPPAAL [START_REF] Behrmann | A tutorial on UPPAAL[END_REF] and simulation using the TASM Toolset [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF]. It is a good way to provide a basis for the Coq mechanization. Finally, we envision the extraction of a complete tool from the mechanization in the future, that is the verified tool chain. Underlying the tool is the formal translational semantics [START_REF] Combemale | Essay on semantics definition in MDE -an instrumented approach for model verification[END_REF][START_REF] Cleenewerck | Separation of concerns in translational semantics for DSLs in model engineering[END_REF][START_REF] Gargantini | A Semantic framework for metamodel-based languages[END_REF] of AADL by a mapping to TASM, namely, the sentences of the target language express the semantics of AADL. To enable the proof of semantics preservation of the model transformation: [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] the informal execution semantics formalized directly using Timed Transition System (TTS), is considered as a reference semantics, because we cannot directly prove that the translational semantics is equivalent with the informal one which is provided by the AADL standard; (2) combining the translational semantics (expressed by the TASM sentences) with the semantics of TASM, we can obtain another way to execute the AADL model, and it is constructed as another TTS; (3) the reference semantics is supposed to be correct, and if there is a simulation equivalence relation between the two TTSs, we say the translation preserves the AADL semantics.

The goal of this paper is to verify the translation from AADL to TASM. The main contributions are as follows: (1) a reference semantics of a subset of AADL is formalized in TTS, including periodic threads, data port communications, mode changes and the behavior annex; (2) a formal translational semantics of the subset of AADL by translating it to TASM; (3) a mechanized proof of the semantics preservation of the transformation from AADL to TASM based on ( 1) and ( 2).

The rest of the paper is organized as follows. Section 2 introduces Timed Transition System and its operations. Section 3 presents an overview of the AADL and the abstract syntax of the chosen subset of AADL. The abstract syntax of TASM is expressed in Section 4. Section 5 presents the two formal semantics of the subset of AADL. Section 6 shows the mechanized proof of semantics preservation. We present some discussion about the model transformation tool prototype AADL2TASM in Section 7. Section 8 discusses the related work, and Section 9 gives some concluding remarks.

Timed Transition Systems

TTS is a well-known model used to express real-time behaviors and is often used to compare semantics equivalence between different real-time specification languages [START_REF] Bérard | Comparison of different semantics for time petri nets[END_REF][START_REF] Bérard | When are timed automata weakly timed bisimilar to time petri nets?[END_REF]. However, there are different definitions and operations on TTS for different uses. For example, some definitions use clock variables to express time in TTS [START_REF] Hune | Timed bisimulation and open maps[END_REF], others express time by associating delays, or time intervals to transitions [START_REF] Henzinger | Temporal proof methodologies for timed transition systems[END_REF]. In this paper, we use a variant of the TTS defined by [START_REF] Bérard | Comparison of different semantics for time petri nets[END_REF][START_REF] Bérard | When are timed automata weakly timed bisimilar to time petri nets?[END_REF], where we add a global state to allow communication through shared variables.

Given a global state S G with its initial set I G and R + the set of nonnegative reals, a TTS is defined as follows.

Definition 1 (Timed Transition Systems). A TTS defined over S G and I G is a tuple Ŵ = S L , I L , , P, → , L such that:

• S L is a set of local states, • I L ⊆ S L is the set of initial local states, • is a finite set of labels, • P is a set of predicates, • →⊆ S × ( ∪ R + ) × S is the transition relation,
• L : S → 2 P is a labeling function, L maps each state to the set of predicates which are true in that state, where S = S G × S L .

We write s ı -→s ′ for (s, ı, s ′ )∈ →. Here s, s ′ are values of the type S, and ı ∈ ( ∪ R + ). There are two kinds of transition relations: discrete and continuous. Continuous transitions are typically required to obey the following properties (∀d, d ′ ∈ R + ):

• 0-delay: s 0 -→s ′ ⇔ s = s ′ , • additivity: s d -→s ′ ∧ s ′ d ′ -→s ′′ ⇒ s d+d ′ -→s ′′ ,
• continuity:

s d+d ′ -→s ′ ⇒ (∃s ′′ )(s d -→s ′′ ∧ s ′′ d ′ -→s ′ ),
• time-determinism:

s d -→s ′ ∧ s d -→s ′′ ⇒ s ′ = s ′′ .
Then, we consider operations on TTS, including synchronous product and simulation equivalence. Synchronous product [START_REF] Arnold | Finite Transition Systems -Semantics of Communicating Systems[END_REF] is used to define the semantics of an AADL model as the composition of the semantics of its constituents. This way, the equivalence proof can be obtained in a compositional way from the correctness of the translation of elementary AADL model elements such as threads, connections and modes.

Definition 2 (Synchronous product). Consider n TTSs over the same alphabet and the global state S G , Ŵ i = S L i , I L i , , P i , → i , L i , i = 1, . . ., n, where the set of predicates P i are supposed to be pair-wise disjoint. The synchronous product is a TTS: Ŵ = i=1,...,n Ŵ i = S L , I L , , P, →, L , such that:

• S L = S L 1 × • • • × S L i × • • • × S L n , • I L = I L 1 × • • • × I L i × • • • × I L n , • P = i=1,. . .,n P i , • → satisfies the following rules: ∀i, (g, l i ) e → i (g ′ , l ′ i ) (g, (l 1 , . . ., l i , . . ., l n )) e →(g ′ , (l ′ 1 , . . ., l ′ i , . . ., l ′ n )) , e ∈ ∀i, (g, l i ) d → i (g ′ , l ′ i ) (g, (l 1 , . . ., l i , . . ., l n )) d →(g ′ , (l ′ 1 , . . ., l ′ i , . . ., l ′ n )) , d ∈ R +
The rules represent that all TTSs make a step at the same time with compatible updates of the global state, and we consider discrete transitions and continuous transitions separately.

• L = {(g, (l 1 , . . ., l n )) → i=1,. . .,n L i (g, l i )}.
Bisimulation and its variants [START_REF] Milner | Communication and Concurrency[END_REF] are usually formulated over TTSs. In this work, what is proved in Coq is strong simulation equivalence which implies ACTL (the universal fragment of Computation Tree Logic) and ECTL (the existential fragment of Computation Tree Logic) preservation [START_REF] Baier | Principles of Model Checking[END_REF] and thus preservation of the UPPAAL query language.

Definition 3 (Strong simulation). Given an alphabet and two TTSs over the two global state S G 1 and

S G 2 , Ŵ 1 = S L 1 , I L 1 , , P, → 1 , L 1 and Ŵ 2 = S L 2 , I L 2 , , P, → 2 , L 2 , we say that Ŵ 2 strongly simulates Ŵ 1 , denoted Ŵ 1 Ŵ 2 , if there exists a relation R ⊆ S 1 × S 2 called a strong simulation relation where S 1 = S G 1 × S L 1 and S 2 = S G 2 × S L 2 , such that: • ∀s 0 1 ∈ I G 1 × I L 1 , there exists s 0 2 ∈ I G 2 × I L 2 , such that (s 0 1 , s 0 2 ) ∈ R, • ∀(s 1 , s 2 ) ∈ R, ∀e ∈ , ∀s ′ 1 such that s 1 e -→ 1 s ′ 1 , there exists s ′ 2 ∈ S 2 such that s 2 e -→ 2 s ′ 2 and (s ′ 1 , s ′ 2 ) ∈ R, • ∀(s 1 , s 2 ) ∈ R, ∀d ∈ R + , ∀s ′ 1 such that s 1 d -→ 1 s ′ 1 , there exists s ′ 2 ∈ S 2 such that s 2 d -→ 2 s ′ 2 and (s ′ 1 , s ′ 2 ) ∈ R, • ∀(s 1 , s 2 ) ∈ R, then L 1 (s 1 ) = L 2 (s 2 ).
Here the simulation relation R is general. It will be specialized when used in the proof (see Section 6). Additionally, discrete transitions and continuous transitions are treated separately.

Definition 4 (Strong simulation equivalence). if Ŵ 1 Ŵ 2 and Ŵ 2 Ŵ 1 , then we say there is a strong simulation equivalence relation between Ŵ 1 and Ŵ 2 , i.e. two-directions strong simulation, noted Ŵ 1 ≃ Ŵ 2 .

A subset of AADL

In this section, we first give an overview of the AADL, and then we elaborate the language subset that we will consider for translation. Finally, the abstract syntax of the considered subset is presented.

Overview of the AADL

AADL describes a system as a hierarchy of software and hardware components. It offers a set of predefined component categories as follows:

• Software components: thread, thread group, subprogram, data and process.

• Hardware components: processor, memory, bus, device, virtual processor and virtual bus.

• System components which represent composite sets of software and hardware components.

A component is given by its type and its implementation. The type specifies the component's external interface in terms of features. Features can be ports, server subprograms or data accesses depending on the chosen communication paradigm. Implementations specify the internal structure of the components in terms of a set of subcomponents, their connections, modes that represent operational states of components, and properties that support specialized architecture analysis.

However, system behaviors do not only rely on the structure defined by the above components but also rely on the runtime environment (like operating system or virtual machine) [START_REF] Feiler | Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language[END_REF]. AADL offers an execution model that covers most of the runtime needs of real-time systems: (1) a set of execution model attributes can be attached to each AADL declaration, such as thread dispatch protocols, communication protocols, scheduling policies, mode change protocols, and partition mechanisms (support of ARINC 653 standard in avionic systems) (Delange et al., 2009), etc.; (2) the semantics of the execution model is also given, namely the execution semantics of AADL.

Moreover, the behavior annex (SAE, 2011) describes more precisely the behaviors of threads and subprograms. The behavior annex has an independent syntax and semantics. So, an AADL model is composed of its structure, its execution model and its behavior annex. Correspondingly, the AADL model transformation and translational semantics, should cover these three aspects [START_REF] Abdoul | AADL execution semantics transformation for formal verification[END_REF].

The considered subset of AADL

AADL execution model mixes synchronous and asynchronous aspects [START_REF] Sae | AS5506A: Architecture Analysis and Design Language[END_REF][START_REF] Franc ¸a | The AADL behaviour annex -experiments and roadmap[END_REF][START_REF] Filali-Amine | Development of a synchronous subset of AADL[END_REF]. A synchronous execution model is obtained by considering logically synchronized periodic threads communicating through data ports. In the asynchronous execution model, it is possible to raise events, to specify sporadic and aperiodic threads, communication through shared variables, and remote procedure calls, etc. As a main difference with the existing approaches, we focus on the verification of the AADL model transformation. However, describing the formal semantics of the whole AADL is a very hard and time consuming task, as well as formally proving the correctness of its translation to another formalism. Thus we have identified a subset and restricted the correctness proof to this subset. In this paper, we consider the synchronous one, including periodic threads, data port communications, mode changes and the behavior annex. This subset is usually used in safety-critical systems, to guarantee the determinism and predictability of system behaviors. Here multi-partitions and multi-processors mechanisms are excluded, and we just consider simple scheduling features: single-processor and non-preemption.

A quick overview of the considered subset of AADL is given, including the structural elements and the execution model attributes. Its execution semantics will be given and formalized in Section 5.

Periodic threads

Based on the modes of the system, a thread may be active, inactive, or halted. In AADL, only active threads can be dispatched and scheduled for execution.

A thread can have input ports and output ports to receive and send messages. AADL defines three types of ports: data, event and event data ports. Event and event data ports support queuing buffers, but data ports only keep the latest data. We consider data ports. However, out event ports used to trigger mode changes are also considered.

AADL supports the classical thread dispatch protocols: Periodic, Aperiodic, Sporadic and Background. Periodic dispatch is the only protocol considered in this paper, and its execution model attribute is expressed as: Dispatch Protocol ⇒Periodic.

Moreover, several properties can be assigned to a periodic thread, such as: period given by the Period property in the form of Period ⇒ 100 ms (i.e. Frequency = 10 Hz), execution time through the Compute Execution Time property or the computation(BCET, WCET) statement of the behavioral annex, and Deadline. By default, when the deadline is not specified it equals the period.

Data port communications

Port connections link ports to enable the exchange of messages among components. In order to ensure deterministic data communication between the data ports of periodic threads, AADL offers two communication protocols: Immediate and Delayed. The execution model attribute is attached to the data ports, and expressed as: Timing ⇒{Immediate, Delayed}.

For an immediate connection, the execution of the recipient thread is suspended until the sending thread completes its execution when the dispatches of sender and receiver threads are simultaneous. For a delayed connection the output of the sending thread is not transferred until the sending thread's deadline, typically the end of the period. Notice that they have not necessarily the same period, which allows over-sampling and under-sampling. A port connection can also be declared with modes specifying whether the connection is part of specific modes or is part of the transition between two specific modes.

Mode change

A mode represents an operational state, which manifests itself as a configuration of contained sub components, connections, and modespecific property values. When multiple modes are declared for a component, a mode state machine identifies which event arrival fires a mode transition, and the new mode. The clause in modes indicates which subcomponents and connections are active in a given mode. Connections can also be active during mode transitions.

An AADL model is a tree of components, and each component has one or more operating modes. Thus, AADL uses the concept of system operation mode (SOM) to define the hierarchical composition of component modes. A SOM is a vector of modes [START_REF] Bertrand | A study of the AADL mode change protocol[END_REF], where each element is associated to a component. If a component is active, the associated element is valued with the current mode of the component. If a component is inactive, the associated element is tagged inactive.

A system has exactly one initial SOM, which is the set of initial modes of each component. SOM transitions define how a system transits from one SOM to another due to some stimulus. SOM transitions can be declared at each level, and extracting them from a set of mode state machines can be based on a breadth-first walk algorithm among the component tree [START_REF] Bertrand | A study of the AADL mode change protocol[END_REF]. When a mode change is requested, a SOM transition is engaged. The new SOM is obtained from the old SOM, by changing the values of the vector elements that are involved in the mode change. In this paper, we mainly consider the relation between SOM transitions and threads/connections.

AADL offers two mode change protocols: Emergency and Planned. They differ on the instant where mode change actually occurs. The execution model attribute is attached to the mode transitions, and expressed as: Mode Transition Response ⇒{Emergency, Planned}. To guarantee determinism, we consider the planned one.

Behavior annex

The behavior annex can be used to describe a set of legal behaviors for a thread or a subprogram. It is described using a transition system with annotated states: initial specifies a start state, return specifies the end of a subprogram, complete specifies completion of a thread, and zero or more intermediate execution states. Transitions define system transitions from a source state to a destination state. Transitions may be guarded by conditions and trigger actions. Conditions and actions include sending or receiving messages, assigning variables and execution abstractions such as use of CPU time or delay, etc. Here, the specification of dispatch conditions for sporadic or aperiodic threads, and shared data communication, which imply loss of determinism, are excluded.

An AADL example. A simplified example of an Electronic Throttle Controller (ETC) (Ouimet et al., 2006) within our chosen subset is given (Fig. 2). A car may cruise automatically or be controlled by the driver at different speeds. The system is split into a system component, a process component (Cruise), and several thread components (wheel, throttle, speed, command, display). We focus on the modes of the process component, which contains two modes (automatic, manual). In the manual mode, the command component reads data from the driver, the throttle computes the voltage used to control the car, and display the speed parameter. When detecting the event a, the process switches to automatic mode. In the automatic mode, the tasks wheel and speed are released, command is deleted, throttle and display continue to execute. The speed component reads the tours of the wheel and computes the speed, then sends it to the throttle for controlling the car. These threads are periodic with data port connections, and each thread has a behavior annex specification. We show the Cruise process and the throttle thread as an example and a part of the textual specification is given in Fig. 3. The behavior of the throttle thread is made very simple here: the computed voltage is the difference between the wanted speed and the current speed.

Abstract syntax of the subset of AADL

We give the abstract syntax of the considered subset: an AADL model contains several threads, connections, and a SOM automaton. Each thread with its behavior annex belongs to a given SOM, and each connection can belong to a SOM or to a SOM transition. Here, the structural elements and the execution model attributes are expressed in an uniform abstract syntax.

Please notice that: (1) DURATION is a predefined type, EXPRESSION describes the expression language used in the annex and is not given here, VALUE is a type describing all possible values stored in ports, BASTATE and SOM are enumerations extracted from the actual AADL model; (2) the action language of the annex being complex, we abstract it as a function computing outputs from the value of its input ports. The CPU consumption of an action is directly modelled as a Time attribute.

Timed Abstract State Machine

In this section, we first introduce the basic concepts of the TASM language, then we give its abstract syntax.

A brief introduction to TASM

TASM extends the Abstract State Machine [START_REF] Börger | The origins and the development of the ASM method for high level system design and analysis[END_REF] to enable the expression of timing and resource consumption. A basic definition of a TASM specification is given as follows:

Definition 5 (A TASM specification). A TASM specification is a pair E, ASM where:

• E = EV, TU, ER is the environment, including:

-EV denotes the Environment Variables, which are the global variables that affect and are updated by machine execution, -TU is the Types of environment variables that include integer, boolean, and user-defined types, -ER is the set of named Resources, ER = {(rn, rs)|rn is a resource name, and rs is the resource size}. Examples of resources include memory, power, bus bandwidth, etc. • ASM = MV, CV, IV, R is a machine, including:

-MV denotes the Monitored Variables, which are the set of environment variables that affect the machine execution, -CV denotes the Controlled Variables, which are the set of environment variables that the machine updates, -IV denotes the Internal Variables, which are the set of local variables, and their scope being limited to the machine where they are defined, -R is the set of Rules, R = { (n, t, RR, r) |n is the rule name; t is the duration of the rule execution, which can take the form of a single value, an interval [t min , t max ], or the keyword next, the "next" construct essentially states that time should elapse until an event of interest occurs, which is especially helpful for a machine which has no enabled rules, but which does not wish to terminate; RR is the resource consumption during the rule execution with the form rn : = rs; r is a rule of the form "if condition then action", where condition is an expression depending on the monitored variables, and action is a set of updates of the controlled variables. We can also use the rule "else then action".}. A restriction on the set of rules is that they are mutually exclusive, that is, only one rule can be executed at each step.

The concepts of hierarchical composition, parallelism, and communication are also supported by TASM. It uses a set of main machines that execute in parallel, to support the specification of parallel behaviors, and provides sub-machine and function-machine calls to support the specification of hierarchical behaviors. Communications are only between main machines and can use channel synchronization and shared variables.

Simply, the semantics of a main machine can be given as follows: read the shared variables, select a rule of which condition is satisfied, wait for the duration of the execution while consuming the resources, and apply the update set. If there are communications with other machines, it also needs to synchronize.

We give a simplified TASM specification of the throttle thread in the example of Section 3 (Fig. 4), and we assume power and memory are consumed during the execution. Rule1 defines the actual execution of the thread. Rule2 is triggered at completion and updates the thread state at the next dispatch. Notice that this TASM translation of an AADL thread is correct only if the thread execution time is exactly known and no other threads have access to the processor. The actual translation will need two TASM machines (see Section 5).

Abstract syntax of TASM

The abstract syntax of TASM is given as follows: In this paper, we use shared variables to achieve communication. P defines the behaviors of a main machine, x : = exp updates the value of the controlled variable x, time specifies the duration of P, resource specifies the resource usage during the execution of P, r is the name of a resource, P ⊕ P is the choice operator that connects several rules within a main machine, P ⊗ P is a synchronous parallel operator which connects statements within rule actions, the statements must not update the same variables, and P||P is a parallel operator which connects main machines. Composition is synchronous if updates are simultaneous, else asynchronous.

P ::= x := exp | skip | if
To get a complete formalization of TASM, an interested reader can refer to (Ouimet and Lundqvist, 2006).

Two formal semantics for the subset of AADL

In order to enable the proof of semantics preservation of the model transformation, the informal execution semantics of the subset of AADL formalized directly using TTS, is considered as a reference semantics, because we cannot directly prove that the translational semantics is equivalent with the informal one which is provided by the AADL standard. As the behavior is explicitly expressed by atomic transitions, the TTS-based semantics is easy to understand. However, TTSs are mainly a mathematical model which cannot be used to automatically verify properties of a given AADL model. TASM-based translational semantics (for verification purpose) is more complex than the TTS-based one, because we need to know the rather complex TASM semantics to understand the translated TASM sentences. In this paper, the TTS-based semantics is supposed to be correct, and it gives a reference expression of AADL semantics which can be compared with the TASM-based translational semantics.

The TTS-based semantics will be defined as a synchronous product of TTSs communicating through a global state (shared variables). For this purpose, each TTS can leave some variables unspecified, and these variables are assigned by other parallel TTSs; other variables will be modified using the record update notation s ′ = s with { • • • }. So, variables not present in the record update and not declared as unspecified are supposed to be unchanged. Furthermore, in order to avoid deadlocks, we suppose that each deadlock state has a default transition which lets all the variables unchanged. Moreover, as communication between TTSs relies on shared variables, discrete labels are not used and considered to be , that is = {}.

As mentioned in Section 3.3, an AADL model (m) contains several threads, connections, and a SOM automaton. Each thread (th) with its behavior annex belongs to a given SOM, and each connection (cn) can belong to a SOM or to a SOM transition (tr). Concretely speaking, the operational semantics of a periodic thread with data port communications is defined as the synchronous product of two TTSs: TTS thread basic and TTS dispatcher , while the computation of the thread will be refined by the behavior annex. For an immediate connection, the execution of the recipient thread is suspended until the sending thread completes its execution when the dispatches of sender and receiver threads are simultaneous. We use an abstract scheduler to manage it and the scheduler only ensures the static alignment of thread execution order implied by the immediate connection. The operational semantics of the scheduler is defined as TTS scheduler . The operational semantics of the SOM automaton is defined as TTS mode change . Thus, the operational semantics of the considered subset of AADL is the composition of a set of TTSs. The definitions of these TTSs will be given later.

Here, we first define the sets S G and I G .

• The global state is defined by the partial valuation of a set of variables. An IportBuffer variable is defined for each input port of each thread.

The sender copies values of output ports to the buffer, and the recipient copies values from the buffer to the input ports. Each IportBuffer is associated to a boolean variable NewData which is true when the input buffer has got the latest data. It is used to guarantee the deadline of the sender occurs before the dispatch of the recipient when they are logically simultaneous and the connection type between them is Delayed. CurrentTime represents the global current time.

• I G = { CurrentMode → Init M ode (m), Activation TH →             th → true | Init M ode (m) ∈ M odes (th ) th → f alse | Init M ode(m) ∈ M odes(th) , Activation CN → cn → true | Init M ode (m) ∈ M odes (cn ) cn → f alse | Init M ode(m) ∈ M odes(cn) , State(th ) → waiting mode, Dispat ch(th ) → f alse, Get CPU(th ) → f alse, Iport(th) { → ip → 0 | ip ∈ Iports(th)}, Oport(th ) { → op → 0 | op ∈ Oports(th )}, IportB uffer(th ) { → ip → 0 | ip ∈ Iports(th )}, NewData(th ) { → ip → true | ip ∈ Iports(th)}, Dispat chTime(th ) → 0, CurrentTime → 0}.
Here, messages exchanged by threads are supposed to be of type Integer.

As the analysis of AADL in Section 3, the translational semantics should take into account the structural aspect, the execution model and the behavior annex. The semantics function has two parts: the mapping of the structural aspect to the TASM environment (such as thread-related variables, connection-related variables, and mode-related variables), and the mapping of the dynamic aspect to the TASM machines (such as the execution of threads, connections, mode change and the behavior annex). The auxiliary functions, for example Trans ThreadData(th) and Trans Thread(th), will be defined later. We will give the informal interpretation, the operational semantics using TTSs, and the translational semantics by translating into TASM of the subset of AADL in a modular manner.

Periodic threads with data port communications

Informal interpretation

The current mode determines the set of threads that are considered active. Only the active threads can be dispatched and scheduled for execution and other threads are in the waiting mode state or the halted state.

Periodic threads. A periodic thread is dispatched periodically, and its inputs received from other threads are frozen at dispatch time (by default), i.e. at time zero of the period. As a result the computation performed by a thread is not affected by the arrival of new inputs. Similarly, the outputs are made available to other threads at completion or deadline time, depending on the connection.

Data port communications between periodic threads. First, the communication affects the input/output timing of the periodic threads. ( 1) For an immediate connection, the execution of the recipient is suspended until the sender completes its execution. As mentioned above, the inputs have been copied at dispatch time, so the recipient needs to replace the old data using the data got from the sender at the start of execution. (2) For a delayed connection, the value from the sender is transmitted at its deadline and is available to the recipient at its next dispatch. The recipient just needs the last dispatch data from the sender. Second, the immediate connection implies a static alignment of thread execution order, i.e., it deals with the scheduling of the sending of messages and the processing of the received messages.

In conclusion, the time line of a periodic thread with data port communications is represented in Fig. 5.

Operational semantics

Now we give the operational semantics of a periodic thread (th) with data port communications, which is defined as the synchronous product of two TTSs: TTS thread basic and TTS dispatcher .

Definition 6 (TTS thread basic ). The basic behavior of a periodic thread (th) with data port communications is a timed transition system defined over S G and I G , that is TTS thread basic = S L , I L , , → where:

• S L = {StartofExeTime(th) : DURATION}.
As mentioned above, for an immediate connection, the execution of the recipient is suspended until the sender completes its execution. So we save the start time of execution of the thread.

• I L = {StartofExeTime(th) → 0}. • = {}.
• → is defined by the following rules, including discrete transitions and continuous transitions. s and s ′ are values of the type S (S = S G × S L ).

The shared variables State(th), Iport(th), Oport(th), IportBuffer(th), NewData(th), DispatchTime(th), and CurrentTime will be modified by this TTS using the schema s ′ = s with { . . . }, while CurrentMode, Activation TH(th), Activation CN(cn), Dispatch(th) and Get CPU(th) are declared as unspecified (namely, they will be modified by other TTSs). We also use the overloading operator <+, which is defined as ACTIVATION. Two rules are used to deal with the relation between the periodic thread th and mode change (in Section 5.3). A shared variable Activation TH(th) : {true, false} is used. ACTIVATION [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] means the thread is in the current mode, while ACTIVATION[2] represents the thread waits to be active. The delay is controlled by the TTS associated to the mode change.

s <+{e → v} = {e ′ → v ′ |(e ′ → v ′ ) ∈ s ∧ e ′ / = e} ∪ {e → v}.
s(State(th )) = waiting mode, s(Activation T H(th )) = true, s ′ = s with {State(th) = waiting dispatch} s -→ s ′ ACT IV AT ION [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] s(State(th )) = waiting mode, s(Activation T H(th

)) = f alse, s ′ = s with {CurrentT ime = s(CurrentT ime) + d} s d -→ s ′ ACT IV AT ION [2]
DISPATCH. The rule DISPATCH [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] represents the dispatch of a thread. On the dispatch event, the input ports are read. For this purpose, we must wait for the data transfer made by the sender threads through delayed connections when their deadline occurs at the same logical time as the dispatch of the recipient thread. This condition is defined by the DelayedSyncCond predicate. As mentioned in Section 3.2, the thread can trigger mode change requests (MCRs) by raising an event. Here we use the same ports for data and event, and say that event is a value satisfying the isEvent predicate. The event buffer can be reset by writing the None value. This is done at dispatch time. The rule DISPATCH [2] represents the thread waits to be dispatched. The delay is controlled by the TTS associated to the dispatcher. WAITING EXE. When the thread is dispatched, its execution is managed by a scheduler. Specially, in presence of immediate connection, the scheduler must ensure that the sender completes before the start of execution of the recipient. Moreover, ports of which incoming connection is immediate must be rewritten. The rule WAITING EXE [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] means that the thread gets CPU, while the rule WAITING EXE [2] represents the thread waits to be scheduled. The delay is controlled by a TTS associated to the scheduler (in Section 5.2). [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] where isImmediate(th, ip) checks if the input port ip of thread th is the destination of an immediate connection. This predicate is defined as follows:

s(State(th

)) = waiting execution, s(Get CP U (th )) = true, s ′ = s with { State(th) = execution, Ipo rt(th ) = s(Ipo rt(th)) < + {ip → s(Ipo rtBuf f er (th , ip)) | is Imme diate(th, ip)}, Startof ExeT ime(th) = s(CurrentT ime) } s -→ s ′ W AIT IN G EXE
∃cn ∈ Connections (m), Dst P ort(cn ) = ip ∧ Connection T ype (cn) = Immediate ∧ ip ∈ Iports(th) s(State(th )) = waiting executio n, s(Get CP U (th)) = f alse, s ′ = s with {CurrentT ime = s(CurrentT ime) + d} s d -→ s ′ W AIT IN G EXE[2]
EXECUTION. Here, the execution is abstracted by a function Computation (Inputs : Iports(th) → VALUE) : Oports(th) → VALUE which consumes CPU time during the interval [BCET, WCET] of the thread, and it will be refined by the AADL behavior annex (in Section 5.4). The rule EXECUTION [START_REF] Ouimet | The TASM toolset: specification, simulation, and formal verification of real-time systems[END_REF] represents that the thread is in the progress of its execution. The rule EXECUTION[2] is used to write the computation results into the output ports of the thread.

s(State(th

)) = executio n, s(CurrentT ime) -s(Sta rto f Exe T ime (th )) + d ≤ W CET (th), s ′ = s with {CurrentT ime = s(CurrentT ime) + d} s d -→ s ′ EXECU T ION [1] s(State(th )) = executio n, BCET (th) ≤ (s(CurrentT ime)- s(Sta rtof Exe T ime (th))) ≤ W CET (th), s ′ = s with {State(th ) = computed, Oport(th ) = op∈Opo rts (th ) Computation ({ip → s(Iport(th)) | ip ∈ Iports(th)}, op) } s -→ s ′ EXECU T ION [2] WRITE IMM DATA.
It is used to copy the data of the output ports of the sender to the IportBuffer of the recipient at the completion time of the sender. This copy is only done when the two threads are dispatched at the same time.

s(State(th

)) = computed, s ′ = s with { IportBuf f er = Ipo rtBuf f er < + {Dst T hread(cn ) → s(Oport(th)) | cn ∈ Conn ections(m) ∧ SrcT hread(cn ) = th ∧ ConnectionT ype(cn) = Immediate ∧ s(DispatchT ime(th )) = s(DispatchT ime(DstT hread(cn))) }, State(th) = completed } s -→ s ′ W RIT E IM M DAT A WAITING DEADLINE.
This rule is used to wait for the deadline (i.e. the period here for the sake of simplicity) of the thread.

W AIT IN G DEADLIN E

Definition 7 (TTS dispatcher ). The behavior of the dispatcher of a periodic thread (th) is a timed transition system defined over S G and I G , that is TTS dispatcher = S L , I L , , → where:

• S L = {WaitNextDispatch(th) : {true, false}}.
Here, an auxiliary variable WaitNextDispatch(th) is used.

• I L = {WaitNextDispatch(th) → false}. • = {}.
• → is defined by the following rules. The shared variables State(th), IportBuffer(th), NewData(th), Dispatch(th) and CurrentTime will be modified by this TTS, while others are declared as unspecified.

DISPATCH THREAD. This rule is used to dispatch the thread, and synchronize with the thread using the shared variable Dispatch(th).

W AIT IN G P ERIOD

REACH PERIOD. This rule represents that the thread arrives at its period. The output of the delay connections is also expressed in this rule, namely, copy the data of the output ports of the sender to the IportBuffer of the recipient at the deadline of the sender. We also set the NewData variable to true in order to indicate the data transfer has been done. The TASM environment associated to each thread is defined as a set of typed variables such as the state and the resource consumption of the thread. Messages exchanged by threads are supposed to be of type Integer. The variables associated to connections are defined as well.

Listing 2 The TASM enviro nme nt of an AADL periodic thread with dat a por t commun ications. ... }

The dynamic behavior of a periodic thread with data port communications is defined as two TASM machines in parallel: TASM Thread(th) and Periodic Dispatcher(th), as shown in Listing 3.

• A periodic thread (th) is expressed by TASM Thread(th) with six rules: Activation, Dispatch, Waiting Execution, Execution, Write Immediate Data, and Waiting Next Event. In the rule Execution, the duration of execution is [BCET,WCET] and processor consumption is 100%. The rule Waiting Next Event is used to deal with the waiting time when activation, dispatch and execution conditions are not satisfied. Additionally, the behavior of a connection is separated in two parts: Read and Write. • The dispatcher of a periodic thread (th) is expressed by Periodic Dispatcher(th) with three rules: Dispatch Thread, Waiting Period, and Waiting Next Event. The rule Waiting Period corresponds to the rules WAITING PERIOD and REACH PERIOD of TTS dispatcher (Definition 7).

According to the TASM semantics (Section 4.1), the system will wait for the duration of the execution of the rule, then apply the update set (i.e. actions). Thus, the TASM-based translational semantics hides implicit behaviors provided by the TASM semantics. Translation rules are written using an ML-like language (close to the Coq notations) with bold font keywords as follows. References to other TASM machines are also bold.

Informal interpretation

As mentioned above, in presence of immediate connection, the scheduler must ensure that the sender completes before the start of execution of the recipient. Here, we give an abstract view of the scheduler. The given behavior allocates the CPU to a waiting thread th of which immediate data emitters that have been synchronously dispatched with th have completed their task.

Operational semantics

Definition 8 (TTS scheduler ). The behavior of the scheduler is a timed transition system defined over S G and I G , that is TTS scheduler = S L , I L , , → where:

• S L =∅. • I L =∅. • = {}.
• → is defined by the following rules. The shared variables Get CPU(th) will be modified by this TTS, while others are declared as unspecified.

ALLOCATE CPU. This rule is used to allocate the CPU to a waiting thread. (2) SOM transition. In this paper, we consider the planned one. Fig. 6 shows the time line of an AADL SOM transition.

At the beginning, the system is in the source mode of a SOM transition (i.e. oldSOM). After a mode change request (MCR) has occurred, execution continues under the oldSOM until the dispatches of a set of critical threads that are active align at their hyper-period (called Hyper(oldSOM)), then the mode transition in progress state is entered. A periodic thread is considered as critical if its Synchronized Component property is true. That means, the duration from the oldSOM state to the mode transition in progress state is the distance to the next hyper-period of these critical threads.

In the mode transition in progress state, some threads enter the new mode (become active), some threads exit the old mode, the critical threads of both new and old modes continue to execute, and the connections belong to oldSOM will be deleted. The system is in the mode transition in progress state for a limited amount of time, which is the distance to a multiple of the hyper-period of the critical threads that continue to execute (called Hyper(newSOM)*). Finally, the system enters the destination mode of the SOM transition (i.e. newSOM).

When a MCR is responded, all of the other incoming MCRs will be ignored, and we don't consider the higher priority requests here.

Operational semantics

Now, we give the operational semantics of the SOM automaton of the AADL model (m).

Definition 9 (TTS mode change ). The behavior of the SOM automaton is a timed transition system defined over S G and I G , that is TTS mode change = S L , I L , , → where:

• S L = ModeTransitionInProgress : {true, false}, GetMCR(tr) : {true, false} .

Here, two auxiliary variables are used.

• I L = ModeTransitionInProgress → false, GetMCR(tr) → false .

• = {}.
• → is defined by the following rules. The shared variables CurrentMode, Activation TH(th), Activation CN(cn), and CurrentTime will be modified by this TTS, while others are declared as unspecified.

GET MCR. This rule gets events sent by threads and selects a corresponding mode transition.

s(CurrentM ode) = SrcM ode(tr), isEvent( s(Opo rt(th , op ))),

M CR T h(tr ) = th, M CR P ort(tr ) = op, s ′ = s with { GetM CR(tr) = true} s -→ s ′ GET M CR ENTER MC PL.
This rule makes a random choice of one of the MCRs, other MCRs are disabled. The system goes to the mode transition in progress state, old threads and connections are deactivated, while new threads are activated.

Activation T H = th → true | Dst M ode (tr ) ∈ M odes (th ) th → f alse | otherwise , Activation CN =             cn → true | SrcM ode (tr ) ∈ M odes (cn ) ∧ Dst M ode (tr) ∈ M odes(cn) cn → f alse | othe rwise , M odeT ransitionInP rogress = true} s -→ s ′ EN T ER M C P L
MC PL. This rule means that the system enters the new SOM.

Behavior annex

AADL supports an input-compute-output model of computation and communication for threads. The input/output timing is defined by the execution model, and the computation can be refined by the behavior annex. So, there is a close relation between the AADL execution model and the behavior annex. The execution model specifies when the behavior annex is executed and on which data it is executed, while the behavior annex acts in a thread (or a subprogram) and describes behaviors more precisely. Thus, the semantics specifications given as above will be enriched by the behavior annex.

Informal interpretation

The behavior annex is described using a transition system in the following form:

annex b e h a v i o r _ s p e c i f i c a t i o n { ** < st ate _var iab les > < initializatio n > < stat es > < transi tions > ** } ;

State Variables represent the variables with the scope of the behavior annex, and they may hold the inputs, the intermediate results, and the outputs. States: initial specifies a start state, return specifies the end of a subprogram, complete specifies completion of a thread, and other states represent intermediate execution steps. Transitions define system transitions from a source state to a destination state. A transition can be guarded with execution conditions. An action part can be attached to a transition and it performs message sending, assignments or time consuming activities. However, the action part is related to the transition and not to the states: if a transition is enabled, the action part is performed and then the current state becomes the transition destination state. When the transition reaches a complete or return state, the thread or the subprogram will be completed.

Operational semantics

The operational semantics of the behavior annex is defined as the refinement of the "Execution" rule of TTS thread basic , where the state S L extends the semantics state of TTS thread basic with CurrentBAState and StartTransitionTime. The initial value of CurrentBAState is the initial state of the behavior annex. StartTransitionTime is used to save the start time of the execution of the transition, and its initial value is the StartofExeTime of the thread.

BA EXECUTION. This rule expresses the execution of each transition of the behavior annex, and the StartTransitionTime is accumulated for each transition. BA COMPLETE. This rule means the execution of the behavior annex is completed. An auxiliary variable isFinal is used to denote the complete state of the behavior annex.

s(State(th )) = executio n, isF inal (s(CurrentBAState)) = true, s ′ = s with {State(th) = computed} s -→ s ′ BA COM P LET E

Translational semantics

The translational semantics specification of the behavior annex contains three parts: structure, guards and actions.

Structure. State Variables are mapped to the TASM environment variables with general types such as integer, real numbers and booleans. States are translated into TASM internal variables. Each transition of the behavior annex is translated into a TASM rule. These rules will take the place of the "Execution" rule of the periodic thread.

In each TASM rule, the condition is built from the current state of the thread (State(th)), the source state of the transition, and the guards of the transition, while the actions of the rule include the actions of the transition and the destination state of the transition.

When all the transitions are translated, a new rule (Behavior Annex Completion) is added. Then the TASM machine executes the next rule (i.e. Write Immediate Data) of the periodic thread.

Guards. The execution conditions which are logical expressions based on the state variables are considered. Here, we do not detail the translation of behavior expressions. The corresponding function is denoted ͠Guard͡.

Actions. We mainly consider the basic actions including message sending, assignments to variables, and timing. ( 1) Message sending is expressed by the assignment of the port variables. (2) Assignments are expressed by the assignment of the corresponding environment variables. (3) The behavior annex introduces the statements computation(min,max) and delay(min,max), which express the use of the CPU and the suspension for a possibly non-deterministic period of time between min and max respectively. They are related to the transitions and not to the states, which is consistent with the TASM semantics. Thus, the timing actions are translated into the duration of the corresponding TASM rule. Here, we use a subset of the proof mechanized by Coq to interpret the idea, which takes into account delayed connections between periodic threads.

Compositional proof methodology

An AADL model can contain several periodic threads. We would like to prove the simulation equivalence between the operational semantics of a thread and its translational semantics in TASM, and then the full semantics will be preserved by using synchronous product in both sides. This method is called as compositional proof and it will reduce the complexity of the proof.

The theorem of simulation of synchronous product is given as follows.

Theorem 1. Let The proof of this theorem relies on the definition of simulation relation, including the correspondence of invInit, invNext, invDelay, simuInit, simuNext, simuDelay, and simuPred.

Applying the compositional principle

Firstly, the abstract syntax and the operational semantics of the subset of AADL, the abstract syntax and the operational semantics of TASM (named MM TTS), and the translation from AADL to TASM are specified in Coq.

Secondly, we prove the following theorems:

Theorem 2. For every periodic thread with delayed connections Th(i), its operational semantics is strongly simulated by its translational semantics into TASM, noted TTS(Th(i)) MM TTS(Trans Thread(Th(i))).

Theorem 3. For every periodic thread with delayed connections Th(i), its translational semantics into TASM is strongly simulated by its operational semantics, noted MM TTS(Trans Thread(Th(i))) TTS(Th(i)).

Here, TTS(Th(i)) is the synchronous product of TTS thread basic and TTS dispatcher defined in Definitions 6 and 7, respectively. Trans Thread(Th(i)) is the parallel composition of TASM Thread(th) and Periodic Dispatcher(th) defined in Listing 3.

The sketch of the proof is shown in Fig. 8. Theorem AADL2TASM simu1 is declared for the direction from AADL to TASM, and Theorem AADL2TASM simu2 is declared for the direction from TASM to AADL. The generic definition of strong simulation is concretized as two instances: SR and SR'.

• In SR, the generic definition of mapping function on states is concretized as A2T: S → {env : Env ; upds : Upds}, namely, according to the state S in the AADL TTS, we can get the corresponding environment Env and the next update set Upds in the TASM TTS; the generic definition of mapping function on predicates is concretized as AP2TP; we also construct invariant instances (getInvariant AADL) on the AADL TTS to restrict to a superset of reachable states. • In SR', the generic definition of mapping function on states is concretized as T2A: Env × mState → S, namely, according to the environment Env in the TASM TTS, we can get the corresponding S in the AADL TTS, some information are given explicitly in the AADL TTS, but they are implicit in the TASM rules, so these information need to be complemented into the TASM TTS (getAuxiliary TASM); the generic definition of mapping function on predicates is concretized as TP2AP; we also construct invariant instances (getInvariant TASM) on the TASM TTS.

The actual definition of A2T and T2A are complex, because they depend on the management of the TASM update set which introduces delays in assignments.

A Coq formalization of a subset of the paper contents restricted to delayed connections can be downloaded at http://www.irit.fr/ Jean-Paul.Bodeveix/COQ/AADL2TASM/V0/. The proof represents about 1200 lines of Coq. The definitions of TTS, synchronous product, simulation relation and some relative lemmas represent 13% of this code. The abstract syntax and formal semantics of both AADL and TASM represent 27% of the code. The transformation from AADL to TASM represents 10% of this code. The rest of the code corresponds to the simulation equivalence proofs (50% of the code).

Towards a verified tool chain

Actually, the first version of the model transformation tool prototype has been implemented in ATL (ATLAS Transformation Language) directly. It is a good way to provide a basis for the Coq mechanization. Finally, we envision the extraction of a complete tool from the mechanization in the future, that is the verified tool chain. Here we present the prototype.

The prototype is named as AADL2TASM. It has been designed as a plug-in of the OSATE modelling environment, as shown in Fig. 9. The model transformation language ATL is used as the automatic transformation engine to express the mapping from AADL models to TASM models. The source meta-model is the standard AADL meta-model, and the destination one is defined using the KM3 language.

The first technique of verification is achieved with UPPAAL by mapping each machine to a timed automaton. Here we reuse the translation principle from TASM to UPPAAL given by the authors of TASM [START_REF] Ouimet | A Formal Framework for Specification-Based Embedded Real-Time System Engineering[END_REF], and implement it using ATL. The verification properties can be expressed by the UPPAAL's query language which is a subset of ACTL ∪ ECTL. Notice that, the behavior annex is an abstraction of the real system behavior where complex data manipulations are replaced by their duration (i.e. Time(BA tr) as shown in Listing 8). Moreover, the translation to UPPAAL accepts the data types that are recognized by UPPAAL (records, arrays, bounded integers, enumerated types). Furthermore, as with any model checking approach, the explored state space must not be too large, so the data usage inside the annex should not be complex. In these contexts, we can verify data related safety, and liveness properties as well as schedulability (through deadlock-detection). Other real-time properties (which need observer automata) will be considered in the future.

The second technique of verification is by using TASM Toolset to analyze the timing sequences and resource consumptions. First, it generates graphs showing the time progression of individual main machines, to perform different kinds of analysis, such as average time consumption and minimal and maximal time consumption regarding a specific rule. Second, it generates graphs showing the aggregate resource consumption for each resource versus the time axis, to calculate the minimum, maximum, and average resource consumption for each resource.

In order to extract a complete verified tool chain, a research perspective is to consider how executable code for dedicated model transformation language such as ATL could be extracted from Coq.

Related work

The AADL description language is a widely used and largely studied standard for the specification of embedded real-time architectures in the avionics and aerospace industry. To extract executable specifications from AADL descriptions in a way suitable for formal verification, one of the easiest ways certainly is to use model transformation technologies, while taking the outmost care to guarantee the preservation of the specification's meaning through the process of its translation in the target modeling framework. et al. (2008) translate most of the AADL concepts into the BIP language, except for the mode change. BIP is a framework for modeling heterogeneous real-time components using three layers: the lower layer describes behaviors, the intermediate layer describes interactions, and the upper layer describes scheduling policies. It provides two categories of verification properties: deadlock detection by using the tool Aldebaran, and some simple timing properties using observers. [START_REF] Rolland | Modes in asynchronous systems[END_REF] translate the AADL models into TLA+. TLA+expresses discrete time only. Moreover, the only tool for TLA+is TLC and it is not very efficient.

AADL model transformations

Chkouri

The translation proposed by [START_REF] Sokolsky | Schedulability analysis of AADL models[END_REF] mainly focus on the schedulability analysis of AADL models, a smaller subset (modes and the behavior annex are excluded) is translated into the real-time process algebra ACSR, and use the ACSR-based tool VERSA to explore the state space of the model, looking for violations of timing requirements. ACSR can express the notation of resource explicit in system models. [START_REF] Abdoul | AADL execution semantics transformation for formal verification[END_REF] translate a behavioral subset, minus mode changes, to IF, where they can analyze some safety properties of the system. The behaviors are, however, not expressed using AADL's behavior annex, but their own behavioral language.

In the work of [START_REF] Berthomieu | Formal verification of AADL specifications in the topcased environment[END_REF], a synchronous subset of AADL with the behavior annex is translated into Fiacre, and then the Fiacre model is compiled into Timed Petri Nets (TPN) for verification. However, the paper does not explain their semantics, and it just presents the translation principle.

In the work of Ölveczky et al. (2010), a subset of AADL is translated into Real-Time Maude, and it provides an AADL simulator and LTL model checking tool called AADL2Maude. Real-Time Maude is a formal real-time rewriting logic.

The translation proposed by [START_REF] Jahier | Virtual execution of AADL models via a translation into synchronous programs[END_REF] covers a subset of AADL except for the behavior annex, and is instead given as a program in the synchronous language Lustre. The translation into Polychrony [START_REF] Ma | Distributed simulation of AADL specifications in a polychronous model of computation[END_REF] mainly focuses on the multi-partitions structure of an embedded architecture and aims at simulating and verifying a GALS (globally asynchronous locally synchronous) model from the given AADL specifications. [START_REF] Monteverde | VTS-based Specification and Verification of Behavioral Properties of AADL Models[END_REF] propose Visual Timed Scenarios (VTS) as a graphical language for the specification of AADL behavioral properties. Then a translation from VTS to Timed Petri Nets is presented. Model-checking of properties expressed in VTS is enabled using TPN-based tools. [START_REF] Rugina | The ADAPT tool: from AADL architectural models to stochastic petri nets through model transformation[END_REF] propose a dependability analysis tool (called ADAPT) on the AADL models. Its input is an AADL model annotated with dependability-related information (through the AADL error model annex), and its output is a dependability evaluation model in the form of a Generalized Stochastic Petri Net (GSPN). The GSPN model can be processed by existing dependability evaluation tools, to compute quantitative measures such as reliability, availability, etc. [START_REF] Bozzano | Safety, dependability and performance analysis of extended AADL models[END_REF][START_REF] Bozzano | A model checker for AADL[END_REF] present a graphical toolset, called the COMPASS platform, for verifying AADL models by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA (Failure Mode and Effects Analysis) tables and dynamic fault trees, to performability evaluation, and diagnosability analysis.

The problem of formally analyzing AADL models is an absolutely crucial problem that has been addressed by a number of research groups recently. Most of those efforts have targeted subsets of the large AADL for "functional analysis", "schedulability analysis", or "dependability analysis", etc. In this work, we consider a behavioral subset for functional analysis. Compared with the existing approaches, the main advantage of TASM is its ability to manage resources. Indeed, now we just consider simple resource information such as processor usage in the transformation. However, all the resource declarations contained in an AADL model can be translated to TASM resources. Their usage could be checked by dedicated predicates. Then it would be possible to verify that a given resource is not overloaded. Furthermore, a formal proof of the semantics preservation of the transformation has not been considered by them. Thus, the novel aspects of this work are the verification of the AADL transformation and the ability to consider resource usage.

The verification methods of model transformations

There are many approaches to gain assurance that the transformation or the translation of a specification or a program is semanticpreserving. This can be done by directly building a theorem-prover-verified compiler [START_REF] Leroy | Mechanized semantics for compiler verification[END_REF][START_REF] Leroy | Formal verification of a realistic compiler[END_REF], by using translation validation [START_REF] Pnueli | Translation validation[END_REF][START_REF] Necula | Translation validation for an optimizing compiler[END_REF], proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF], semantics-anchoring method [START_REF] Chen | Semantic anchoring with model transformations[END_REF][START_REF] Narayanan | Using semantic anchoring to verify behavior preservation in graph transformations[END_REF], etc.

A verified compiler is one specified with a theorem prover to formally check that its transformation algorithm defines a perfect match between the semantics of the source and target languages. This is the approach adopted in this paper.

Translation validation consists of using software model-checking techniques to verify the equivalence between a program and its translation.

Proof-carrying consists of returning the transformed program together with a proof of its correctness (the traces of deductions which yield the program) and to check that proof afterwards.

Semantics anchoring is a technique to specify the semantics of DSMLs (Domain Specific Modeling Languages). It relies on the observation that the semantics of DSMLs can be represented by a small set of semantics units such as FSMs (Finite State Machines), Timed Automata, etc., and these semantics units have a common semantics framework, that is ASMs (Abstract State Machines). Based on the semantics-anchoring method, the source and target models can be transformed to the semantics unit respectively, thus verify their equivalence.

Except for semantics preservation, there is another viewpoint for the verification of model transformations, such as the work of [START_REF] Guerra | Automated verification of model transformations based on visual contracts[END_REF] and [START_REF] Kessentini | Example-based model-transformation testing[END_REF]. They verify some transformation requirements or properties on the execution of actual model transformations written by a dedicated language like ATL, QVT or Kermeta. [START_REF] Lin | A testing framework for model transformations[END_REF] and [START_REF] Mottu | Model transformation testing: oracle issue[END_REF] research model transformation testing methods. [START_REF] Cariou | OCL contracts for the verification of model transformations[END_REF] propose to specify model transformation using pre and post conditions on the source and target meta-model expressed using OCL (Object Constraint Language) constraints. [START_REF] Cabot | Verification and validation of declarative model-to-model transformations through invariants[END_REF] propose verification and validation techniques for model-to-model transformations based on the analysis of a set of OCL invariants automatically derived from the declarative description of the transformations. These invariants state the conditions that must hold between a source and a target model in order to satisfy the transformation definition, i.e. in order to represent a valid mapping.

In the area of AADL research, the related work always use manual validation. The work of [START_REF] Bodeveix | Towards formalising AADL in proof assistants[END_REF] formalizes a subset of the AADL meta-model using the B specification language and the Isabelle proof assistant in order to prove transformations of AADL models correct. Filali-Amine and Lawall (2010) define a refinement of a synchronous subset of AADL using the Event B method, and give simplified proof obligations. [START_REF] Bertrand | A study of the AADL mode change protocol[END_REF] translate the AADL mode change protocol into Timed Petri Nets, and verify some properties to validate the proposed translation. Another way is to compare alternative semantics for the same language. In one of our preview work [START_REF] Pi | A comparative study of FIACRE and TASM to define AADL real time concepts[END_REF], we present a comparative study of Fiacre and TASM to define an AADL subset.

Conclusion and future work

We have presented a translation of AADL into TASM and a methodology to prove the semantics preservation under the assumption that the reference semantics expressed in TTS are correct. However, giving two semantics, the TTS-based one and the translational-based one, which are proved to be equivalent, increases the confidence on the interpretation of the informal semantics. Generally, we hope the idea, i.e., writing a prototype first, doing mechanization based on the prototype and then extracting a verified model transformation tool from the mechanization, can be common to other model to model transformation processes.

The subset of AADL we consider includes periodic threads, data port communications, mode changes and the behavior annex. First, the reference semantics is formalized as a TTS. Second, the translational semantics is formalized by a family of semantics function which inductively associates a TASM fragment with each AADL construct. Third, the theorems and proof of simulation equivalence between the two formal semantics are mechanized by the Coq proof assistant. Our formal semantics and proof of semantics preservation for AADL is an important contribution to the use of AADL for developing safety-critical applications.

Our experience is encouraging, but much more work remains ahead. Firstly, increasingly larger AADL subsets should be formalized to achieve the goal of giving a formal semantics to the entire AADL standard and having verification and simulation tools for AADL models based on such semantics. For example, a larger subset including such as sporadic and aperiodic thread, event port, event data port, data component, complex scheduling, etc., has been considered in our tool prototype. We will consider this larger subset in the formal proof part in future.

Secondly, in this paper, we just consider simple resource information in the transformation. However, all the resource declaration in the AADL models can be translated to TASM resources. Their usage could be checked by dedicated predicates. Then it would be possible to verify that a given resource is not overloaded. To add such capability, we will extend the definition of TTS with resource information. Intuitionally, the resource properties are also preserved during the transformation.

Thirdly, we will consider how executable code for dedicated model transformation language such as ATL could be extracted from Coq.

Fig. 1 .

 1 Fig. 1. A global view of the verified AADL model transformation.

Fig. 2 .

 2 Fig. 2. Architecture of the electronic throttle controller system.

Listing 1

 1 The abstract syntax of the synchronous subset of AADL. Type Thread:= { Iports: set of PORT; \ * Input Ports * \ Oports: se t of PO RT; \ * Output Ports * \ Period: DURATION; BCET: DUR ATION; WCET: DUR ATION; Deadli ne: DUR ATION; Behavior : Be haviorAnnex; Modes: set of SOM; } Type Conn ection:= { SrcThread: Thread; \ * Sourc e Thread * \ DstThread: Thread; \ * Desti natio n Thread * \ Src Port : PO RT; \ * Sourc e Port * \ DstPort: PO RT; \ * Desti natio n Port * \ ConnectionType: {Immediate, Delayed}; Modes: set of SOM; } Type Be haviorAnnex:= { States : se t of BA STATE; Tra nsitions: set of BA Transition; } Type BA Tra nsitio n:= { Src State: BA STATE; \ * Sourc e State * \ DstState : BA STATE; \ * Destination State * \ Time: DUR ATION; Guar d: EXPRESSION; Computation:((Iports(th) → VALUE) × Oports(th)) → VALUE; } Type SOM Tra nsitio n:= { Src Mode: SOM; \ * Sourc e Mode * \ DstMode: SOM; \ * Desti nation Mode * \ MCR Th: Thread; MCR Port: Oports(MCR Th); } Type Model:= { Threads: se t of Thread; Connections: se t of Conn ection; Initial Mode: SOM; Mode Transitions: set of SOM Transition; }

  Fig. 3. A part of textual specification of the AADL model of the ETC system.

  Fig. 4. A TASM example.

  Bexp then P | else then P | time (t min , t max ) ⊲ P | time next ⊲ P | resource r (r min , r max ) ⊲ P | P ⊕ P | P ⊗ P TASM ::= E, P||P||• • •||P

S

  G = { CurrentMode : SOM, Activation TH(th ) : {true , f alse }, Activation CN(cn ) : {true , f alse }, State(th) : { waiting mode, waiting dispatch, waiting executio n, executio n, computed , comp leted }, Dispat ch(th ) : {true , f alse }, Get CPU(th) : {true, f alse}, Iport(th ) : Iports(th ) → V AL U E, Oport(th ) : Oports(th ) → V AL U E, IportB uffer(th ) : Iports(th ) → V AL U E, NewData(th ) : Iports(th ) → {true , f alse}, Dispat chTime(th ) : DU RAT ION, CurrentTime : DU RAT ION }.

  odeData, th∈T hreads(m) T rans T hread(th) ( th∈T hreads(m) T rans BehaviorAnnex(th)) ( cn∈Connections (m) T rans Connection(cn)) Trans Scheduler T rans M ode

Fig. 5 .

 5 Fig. 5. The time line of an AADL periodic thread with data port communications.

  s(State(th )) = waiting dispatch, s(Dispatch(th )) = true, DelayedS yncCond (th, s), s ′ = s with { State(th ) = waiting executio n, DispatchT ime (th ) = s(CurrentT ime ), Ipo rt(th ) = {ip → s(Ipo rtBuf f er (th , ip)) | ip ∈ Iports(th)}, ip∈Iports(th) N ewData(th , ip ) = f alse, op∈Oports(th)|isEvent(s(Oport(th,op))) Opo rt(th , op ) = N one } s -→ s ′ DISP AT CH[1] where Del ayedSyncCond(th , s) ≡ ∀cn ∈ Connections (m), s(Dispatch T ime (SrcT hread(cn)) ) + P eriod (SrcT hread(cn )) = s(CurrentT ime) ∧ DstT hread(cn) = th ∧ Connection T ype (cn ) = Delayed ⇒ s(N ewData(th, DstP ort(cn))) = true s(State(th )) = waiting dispatch, s(Dispatch(th )) = f alse, s ′ = s with {CurrentT ime = s(CurrentT ime)

  s(State(th )) = completed, s(Get CP U (th )) = f alse, s(CurrentT ime) + d ≤ s(DispatchT ime(th)) + P eriod(th), s ′ = s with {CurrentT ime = s(CurrentT ime) + d} s d -→ s ′

  s(Activation T H(th)) = true, s(State(th )) = waiting dispatch, s(Dispatch(th )) = f alse, s ′ = s with {Dispatch(th) = true, W aitN extDispatch(th) = true} s -→ s ′ DISP AT CH T HREAD WAITING PERIOD. This rule does nothing, and it is just used to wait the period of the thread. s(W ait N ext Dispatch(th )) = true, s(CurrentT ime) + d ≤ s(Dis patchT ime(th )) + P eriod(th ), s ′ = s with {CurrentT ime = s(CurrentT ime) + d} s d -→ s ′

  s(W ait N ext Dispatch(th )) = true, s(CurrentT ime) = s(DispatchT ime(th))+ P eriod(th), s ′ = s with { State(th ) = waiting mode, W ait N ext Dispatch(th ) = f alse, Dispatch(th) = f alse, Ipo rtBuf f er = Ipo rtBuf f er < + {DstT hread(cn) → s(Oport(th))} | isDelayOut(th), N ewData(DstT hread(cn)) = true } s -→ s ′ REACH P ERIODwhere isDelayOut(th) checks if the thread th is the source thread of a delayed connection. This predicate is defined as follows:∃cn ∈ Connections(m), SrcT hread (cn ) = th ∧ ConnectionT ype(cn) = DelayedWAIT. This rule is used to deal with the waiting time when the conditions of other rules are not satisfied.s(Activation T H(th)) = f alse, s ′ = s with {CurrentT ime = s(CurrentT ime)

  ip:=IportBuffer(th,ip) Trans Connection Write Imm(th)= ⊗ op ∈ Opo rts (th ) ∧cn ∈ Connectio ns(m) ∧SrcP ort(cn ) = op ∧ConnectionT ype(cn) = Immediate IportBuffer(DstThread(cn),DstPort(cn)):=op Trans Connection Write Delay(th)= ⊗ op ∈ Opo rts (th ) ∧cn ∈ Connectio ns(m) ∧SrcP ort(cn ) = op ∧ConnectionT ype(cn) = Delayed IportBuffer(DstThread(cn),DstPort(cn)):=op 5.2. Scheduler

  s(State(th )) = waiting execution, ∀th ′ ∈ T hreads(m) s(Get CP U (th ′ )) = f alse, ∀cn ∈ Connectio ns(m) Connectio nT ype (cn ) = Immediate ∧DstP ort(cn) ∈ Iports(th) ∧s(DispatchT ime (th )) = s(Dispatch T ime (SrcT hread(cn))) → s(State(SrcT hread(cn))) ∈ {comp leted, waiting mode}, s ′ = s with {Get CP U (th) = true} s -→ s ′ ALLOCAT E CP U FREE CPU. This rule frees the CPU allocated to a thread which has completed its task. s(Get CP U (th )) = true, s(State(th )) = completed, s ′ = s with {Get CP U (th) = f alse} s -→ s ′ F REE CP U 5.2.3. Translational semantics The scheduler should avoid giving the processor to several threads at the same time. Its behavior is defined as a TASM machine with three rules: Allocate CPU, Free CPU, and Waiting Next Event. Listing 4 The TASM ma chine of the scheduler. Trans Scheduler= // Rule Allocate CPU Time 0 (if State(th)=waiting exec ution ∧ th ′ ∈T hreads(m) Conn ectio nT ype (cn ) = Immediate ∧ Dst P ort(cn ) ∈ Ipo rts (th) ∧ Dispatch T ime (th ) = Dis patch T ime (SrcT hread(cn)) ∧ State (SrcT hread(cn)) State(th)=completed and Get CPU(th)=true then Get CPU(th):=false ⊕ //Rule Waiting Next Event Time next (else then skip) 5.3. Mode change 5.3.1. Informal interpretation The behaviors of a SOM transition. The AADL mode change protocol comprises two phases: (1) waiting SOM transition;

Fig. 6 .

 6 Fig. 6. The time line of an AADL SOM transition.

  s(CurrentM ode) = SrcM ode(tr), s(GetM CR(tr )) = true, s(CurrentT ime) mo d Hyper(CurrentM ode ) = 0, s(M odeT ransitionInP rogress) = f alse, s ′ = s with { GetM CR = {tr ′ → (tr = tr ′ )},

  s(M ode T ransitionInP rogress) = true, s(GetM CR(tr )) = true, s(CurrentT ime) mod Hyper(DstM ode(tr)) = 0, s ′ = s with { CurrentM ode = Dst M ode (tr ), → true | Dst M ode (tr ) ∈ M odes(cn) cn → f alse | othe rwise , M ode T ransitionInP rogress = f alse, GetM CR(tr) = f alse} s -→ s ′ M C P L 5.3.3. Translational semantics In the TASM environment, we introduce the CurrentMode variable valued in the set of SOM, and two booleans ArriveHyperPeriod and ModeTransitionInProgress. Listing 5 The TASM environment of the SOM automaton. Trans ModeData= { CurrentMode: SOM; ArriveHyper Peri od: SOM → Boolean; ModeTransitionInProgress: Boolean; ... } The dynamic behavior of the SOM automaton is defined as two TASM machines in parallel: SOM Transition and Manage Hyper(mode). • The basic behavior of the SOM automaton is expressed by SOM Transition with three rules: Get MCR, Mode Transition In Progress and Mode Transition. The machine uses the shared variable Activation TH(th) to synchronize with the execution of periodic threads. The rule Get MCR gets events sent by threads and selects a corresponding mode transition. The rule Mode Transition In Progress expresses the behavior when waiting for the actual SOM transition after a MCR. The rule Mode Transition expresses the actual SOM transition. • We use the machine Manage Hyper(mode) to manage the time Hyper(oldSOM) and Hyper(newSOM)*. Listing 6 The TASM machines of the SOM automaton. Trans Mode = LET SOM Transition=⊕ tr ( LET oldSOM=Src Mode(tr) AND newSOM=DstMode(tr) IN //Rule Ge t MCR time 0 (if CurrentMode=oldS OM and isEvent(O port(MCR Th(tr), MCR Port(tr)))=true then GetMCR(tr):=tr ue) ⊕ //R ule Mode Tra nsitio n In Progress time 0 (if CurrentMode=oldS OM and Get MCR(tr)=tr ue and Arri veHyper Period(oldS OM)=tr ue and ModeTra nsitionIn Progress=fals e then ⊗ tr ′ =tr GetMCR(tr'):=false ⊗ ModeTra nsitionInProgress:=tr ue ⊗ ArriveHyperPeriod(newSOM):=false ⊗ ⊗ th|newSOM ∈M odes(th )\old SOM ∈M odes(th) Activation TH(th):=true ⊗ ⊗ th|oldSOM ∈M odes(th )\ne wSOM ∈M odes(th) Activation TH(th):=false ⊗ ⊗ cn|old SOM ∈M odes(cn)\newSOM ∈M odes(cn) Activation CN(cn):=false) ⊕ //Rule Mode Transition time 0 (if GetMCR(tr)=true and ModeTra nsitionInProgress=tr ue and ArriveHy per Period(new SOM)=true then CurrentMode:=newSOM ⊗ ⊗ cn|ne wSOM ∈M odes(cn )\old SOM ∈M odes (cn ) Activation CN(cn):=true ⊗ ModeTra nsitionInProgress:=false ⊗ ArriveHyperPeriod(oldSOM):=false ⊗ GetMCR(tr):=false) AND Manage Hy per(mode)= time Hyper(mode) (if true then ArriveHyper Peri od(m ode):=tr ue) IN SOM Transition ( mode∈SOM Manage Hyper(mode))

  s(State(th )) = executio n, s(CurrentBAState) = SrcState(BA tr ), s(CurrentT ime) = s(StartT ransitionT ime) + T ime(BA tr), s ′ = s with { CurrentBAState = Dst State(BA tr ), Oport(th ) = Action(BA tr)( Ipo rt(th)) , StartT ransitionT ime = s(CurrentT ime)} s -→ s ′ BA EXECU T ION if Guard(BA tr)=true, ∀BA tr ∈ Transitions(BA) ∧ BA = Behavior(th)

Fig. 8 .

 8 Fig. 8. The proof sketch of the strong simulation equivalence.

  i ) be the synchronous product of TTS(A i ), and i=1,...,n TTS(B i ) be the synchronous product of TTS(B i ). If ∀iTTS(A i ) TTS(B i ), then

Fig. 9 .

 9 Fig. 9. The model transformation tool prototype AADL2TASM.

  • LET name = P AND . . . IN TASM. • IF condition THEN P ELSE P.

	AND Peri odic Dis pat cher(t h)=
	//Rule Dis pat ch Thread
	time 0 (if Acti vation TH(th)=true and State(th)=waiting dispatch
	and Dispat ch(t h)=fals e then
	Dispat ch(t h):=tr ue ⊗ WaitNextDispatch(th):=true)
	⊕ //R ule Waiti ng Period
	time Period(t h) (i f WaitNextDis pat ch(t h)=tr ue then
	WaitNextDis pat ch(t h):=false
	⊗ Trans Connection Write Delay(th)
	⊗ State(th):=waiting mode
	⊗ Dis pat ch(t h):=false)
	⊕ //R ule Waiti ng Next Event
	time next (else then
	skip)
	IN TASM Thread(t h) Peri od Dis patcher(th)
	Trans Connection Read(th)= ⊗
	ip ∈ Ipo rts (th )
	∧cn ∈ Connectio ns(m)
	∧DstP ort(cn ) = ip
	∧ConnectionT ype(cn) = Immediate
	Listing 3 The TASM ma chines of an AADL periodic thread with
	dat a por t communications.
	Trans Thread(th)=
	LET TASM Thread(t h)=
	// Rule Activation
	Time 0 (if State(th)= waiting mode and Activation TH(th)=true then
	State(th):=waiting dispatch)
	⊕ //Rule Dis pat ch
	Time 0 (if State(th)= waiting dis pat ch and Dispatch(th)=true then
	State(th):=waiting exec ution
	⊗ Iport(th):=IportBuffer(th)
	⊗	⊗	Oport(th,op):= None)
	op∈Oports(th)|isEvent(Oport(th,op))
	⊕ //Rule Waiting Exec ution
	Time 0 (if State(th)=waiting executio n and Get CPU(t h)=tr ue then
	State(th):=execution ⊗ Trans Connection Read(th))
	⊕ //Rule Exec ution
	Time (BCET(th), WCET(th)) Resourc e Processor 100
	(if State(th)=exec ution then
	Oport(th):=Compu tation(Iport(th)) ⊗ State(th):=computed)
	⊕ //Rule Write Immediate Data
	Time 0 (if State(th)=compute d then
	State(th):=completed ⊗ Trans Connection Write Imm(th))
	⊕ //Rule Waiting Next Event
	Time next (else then
	skip)

In the TASM environment, we introduce the CurrentBAState variable valued in the set of states of the behavior annex and two booleans: isInitial and isFinal.

Acknowledgements

We would like to thank the anonymous referees for their comments that helped to substantially improve the quality of the paper. Zhibin Yang would like to thank Mr. Mamoun Filali at IRIT for many help and suggestions.

This work was supported in part by the National Natural Science Foundation of China (Grant Nos. 61073013, 61003017), the Aviation Science Foundation of China under Grant 2012ZC51025, the TOPCASED Project, and the RTRA STAE Foundation in France (http://www.fondation-stae.net/).

Listing 7 The TASM enviro nme nt of the behavior annex of a periodic thread. Trans BehaviorAnnexData(th)= { CurrentBAState: BAState; isInitial: BA State → Boolean; isFinal: BAState → Boolean; ... }

We consider all the transitions of the behavior annex of a periodic thread, and the basic semantics specification is presented in Listing 8. It can be detailed when more complex guards and actions are considered.

Listing 8 The TASM rule s of the behavior annex of a periodic thread.

The proof of semantics preservation

In this section, we give the main idea of the proof of semantics preservation of the transformation from AADL to TASM, i.e. the exact correspondence between execution steps defined by the AADL operational semantics and those defined by the semantics of the target TASM model. Here, the semantics preservation is defined as a strong-simulation equivalence between the TTSs related to the AADL model and to the TASM model respectively, which implies ACTL (the universal fragment of Computation Tree Logic) and ECTL (the existential fragment of Computation Tree Logic) preservation and thus preservation of the UPPAAL query language. After a brief introduction to Coq, we introduce the property language used to express atomic observers. Then, we introduce a generic definition of simulation equivalence based on a mapping function on states and a mapping function on predicates. At last, simulation equivalence is applied in a compositional manner on AADL and the obtained TASM models.

A brief introduction to Coq

Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development (CoqArt: The Calculus of Inductive Constructions)[END_REF]) is a theorem prover based on the Calculus of Inductive Constructions which is a variant of type theory, following the "Curry-Howard Isomorphism" paradigm, enriched with support for inductive and co-inductive definitions of data types and predicates. From the specification perspective, Coq offers a rich specification language to define problems and state theorems. From the proof perspective, proofs are developed interactively using tactics, which can reduce the workload of the users. Moreover, the type-checking performed by Coq is the key point of proof verification.

Here, we try to give an intuitive introduction to the Coq terminologies which are used in this paper. In the spirit of "Curry-Howard Isomorphism" paradigm, types may represent programming data-types or logical propositions. So, the Coq objects used in this paper can be sorted into two categories: the Type sort and the Prop sort:

• Type is the sort for data types and mathematical structures, i.e. well-formed types or structures are of type Type. Data types can be basic types such as nat, bool, nat → nat, etc., and can be Inductive structures or Record. We use Fixpoint definitions to define functions over inductive data types. • Prop is the sort for propositions, i.e. well-formed propositions are of type Prop. We can define new predicates using Inductive and Record (for conjunctions of properties).

Properties

In order to express complex properties on the models, we first introduce the atomic observers (Predicate) as for example "port p of thread th has value v", "thread th is in the given state s", and "thread th gets the CPU". From these observers, we build propositional formulas (LP), and give their semantics over the TTS states (through the LPSat function).

We now give the corresponding Coq definitions: Variable S t a t e : Type . Variable Sa t : S t a t e → P r e d i c a t e → Prop . Fixpoin t LP Sat s t f :

Variable

Complex properties expressed using such as LTL, CTL, ACTL and ECTL logics are built from these atomic observers. In order to automatically verify them, the high-level model (AADL) is transformed into the lower-level model (TASM) which can be checked and so that properties are preserved. We consider the ACTL and ECTL logics, which are preserved through the simulation equivalence.

Simulation equivalence

Here, we just give a generic definition of strong simulation between two TTSs named TTS A (abstract semantics) and TTS C (concrete semantics) respectively, including a mapping function on states and a mapping function on predicates. It will be concretized as two instances in the proof, one for each direction (Section 6.4).

Mapping function on states

We introduce a rather complex definition of a mapping between the set of states (StateC) of TTS C and the set of states (StateA) of TTS A. However, in order to build the image of abstract state, some other information may be needed. For this purpose, we introduce an auxiliary state (mState) and define its evolution (mInit, mNext and mDelay).

Consequently, a generic definition of the mapping function on states is defined in Coq as follows:

Recor d ma pping :

Mapping function on predicates

During the model transformation, atomic observers defined on the StateC must be expressed using a formula defined with atomic observers over StateA (the p2lp function). This transformation is extended (LPTransfo) to any complex formula (f) over StateC.

The corresponding Coq definition is given as follows:

Pred2 p 2 l p f 1 ) end .

Strong simulation

We now introduce the definition of strong simulation. It is based on the mapping function on states and the mapping function on predicates. The simulation relation takes as parameters the functions tra and trc which translate common observers (defined by Pred)