Ajinkya Bhave
email: ajinkya@|garlan@cs.|krogh@ece.|arajhans@ece.|schmerl@cs.cmu.edu

David Garlan

Bruce H Krogh

Akshay Rajhans

Bradley Schmerl

Augmenting Software Architectures with Physical Components

Keywords: Software Architecture, Embedded, Control, Physical Modelling

This paper presents an extension of existing software architecture tools to model physical systems, their interconnections, and the interactions between physical and cyber components. We introduce a new cyber-physical system (CPS) architectural style to support the construction of architectural descriptions of complete systems and to serve as the reference context for analysis and evaluation of design alternatives using existing model-based tools. The implementation of the CPS architectural style in AcmeStudio includes behavioral annotations on components and connectors using either finite state processes (FSP) or linear hybrid automata (LHA) with plug-ins to perform behavior analysis. The application of the CPS architectural style is illustrated for the STARMAC quadrotor.

Introduction

Today's models and methods for analysis and design of embedded control systems are typically fragmented along lines defined by disparate mathematical formalisms and dissimilar methodologies in engineering and computer science. While separation of concerns is needed for tractability, such analytical approaches often impose an early separation between the cyber and physical features of the system design, making it difficult to assess the impacts and tradeoffs of alternatives that cut across the boundaries between these domains. This paper concerns extensions of software architectures to include the physical elements of embedded control systems.

Architectures typically represent systems at a higher level than simulation models, which represent the details of a particular system implementation. Although architectural modeling has been used in specific domains to incorporate physical elements as components, there is currently no way of treating cyber and physical elements equally in a general fashion. This is because the vocabulary is inadequate for representing physical components and their interactions with computational elements in embedded control systems and other cyber-physical systems (CPS). Our goal is to create a CPS architectural style as a comprehensive framework for using diverse models and tools for analysis and design of cyberphysical systems.

As a system is being designed, engineers typically want to expose some aspects of a system while abstracting away details of other aspects of the system. From an architectural perspective, when the system is modeled for analysis using a particular formalism, the model typically reflects a structural view of the system that differs from the detailed architecture in some respects. In some cases, one may even want to use a different architectural style to represent an analysis or simulation model in terms of components and connectors. This leads to the need to support different architectural views of the modeled system. In this paper the relationships of heterogeneous models to the CPS architecture are developed by formalizing the structure of each model as an architecture in its own right, which is then associated to the CPS architecture as a particular view of the system.

The following section describes related work in this area. Section 3 motivates the need for a unifying framework augmented with physical components and multiple system views. Section 4 introduces the CPS architectural style. Section 5 describes an example quadrotor system whose architectural description in the CPS style in presented in Section 6. Section 7 presents two models of the quadrotor in different formalisms as architectural views. Section 8 outlines how analyses can be carried out using appropriate plugins in the architecture design tool Ac-meStudio. Section 9 summarizes the contributions of this paper and discusses directions for future work.

Related Work

Over the past decade software architecture has emerged as one of the primary techniques for disciplined engineering of large-scale software systems. Software architecture typically models a system as a graph of components and connectors in which the components represent principal computational elements of a system's run-time structure and the connectors represent the pathways of communication between components [START_REF] Allen | A formal basis for architectural connection[END_REF]. These elements are annotated with properties that characterize their abstract behavior and facilitate reasoning about system-level design tradeoffs. There has been considerable research and development in Architecture Description Languages (ADLs) and tools to support their analysis and realization as code [START_REF] Magee | Concurrency: State Models and Java Programming[END_REF]. Standardized notations such as UML 2.0 [START_REF] Booch | The Unified Modeling Language Reference Manual, Second Edition[END_REF], SysML [START_REF]SysML Home Page[END_REF] and AADL [START_REF] Hudak | Developing AADL models for control systems: A practitioner's guide[END_REF] provide modeling vocabularies of components, connectors and properties. These notations are supported by tools that provide graphical editing and viewing, hierarchical development [START_REF] Moriconi | Introduction to SADL 1.0: a language for specifying software architecture hierarchies[END_REF], checking for component compatibility or substitutability [START_REF] Allen | A formal basis for architectural connection[END_REF], and evaluation of quality attributes such as performance, reliability, and security. Software architectures also support reuse of design expertise and code infrastructure and have been used effectively for a number of embedded control applications [START_REF] Binns | Formal real-time architecture specification and analysis[END_REF][START_REF] Hudak | Developing AADL models for control systems: A practitioner's guide[END_REF].

There are also a number of tools for modeling and simulating physical systems. For example, Modelica is a popular object-oriented, open-standard language for constructing component-based models of physical systems [24]. MapleSim is a tool for developing models of physical systems and generating efficient code for real-time simulations, particularly for hardware-inthe-loop testing [START_REF]MapleSim from Maplesoft[END_REF]. In contrast to the signal flow semantics used in control system modeling, compositions of physical systems are most naturally modeled using acausal connections, which are symmetric reaction relations for which the directionality of interaction flows is determined by the internal state of the interconnected components. Making connections between physical modeling tools and control-oriented modeling frameworks has become an important goal for model-based development (MBD), particularly for avionics systems [START_REF] Verzichelli | Development of an Aircraft and Landing Gears Model with Steering System in Modelica-Dymola[END_REF]. MathWorks has introduced Simscape, a textual MATLAB-based modeling language and Simulink block set that makes it possible to integrate physical models with control-oriented simulations [START_REF]Simscape from Mathworks[END_REF].

There has been an effort to integrate UML/SysML and Modelica to provide support for modeling and simulating continuous dynamics [START_REF] Johnson | Integrating models and simulations of continuous dynamics into SysML[END_REF]. The UML profile called ModelicaML enables users to depict a Modelica simulation model graphically alongside UML/ SysML information models. The ModelicaML profile reuses several UML and SysML constructs, and also introduces new language constructs to specify equations. Similar work has been done for UML and Simulink [START_REF] Shi | Combined usage of UML and Simulink in the design of embedded systems: Investigating Scenarios and Structural and Behavioral Mapping. 4th workshop of Object-oriented Modeling of Embedded Realtime Systems[END_REF]. None of these approaches uses physical components and their interconnections, however, to capture the physical interactions between system components and the emergent dynamic behavior.

Rather than developing a universal modeling syntax and semantics or a meta-modeling framework for translating models between tools, our approach is to relate models and verification results at the architectural level, a level of abstraction that captures the structure of the system without attempting to compre-hend all of the details of any particular modeling formalism.

Need for physical architectural concepts

Although architectural modeling has been used in limited ways to support the incorporation of physical elements as components [START_REF] Reeves | Software architecture themes in JPL's mission data system[END_REF], it currently does not have adequate ways of placing cyber and physical elements on the same footing. This is because software architectures have an impoverished vocabulary for the types of physical components found in cyberphysical systems, the interconnections that determine the interactions between physical components and between cyber components, and the behaviors of physical entities.

Figure 1 shows an AADL representation of a flight computer interfacing with a landing gear [START_REF] Chkouri | Translating AADL into BIP -Application to the Verification of Real-time Systems[END_REF]. Each component represents an AADL thread, with interconnections representing the communication of events or data. The Landing_Gear thread defines the behavior of the physical subsystem in terms of the events generated in response to pilot commands. This architectural description of the landing gear does not go beyond defining the data/signal interface of the controller to the sensors and actuators of the plant. The AADL component view of the gear resembles a black box for the system designer. There is no information about how the gear's subsystems are physically interconnected, or any representation of the controller's assumptions about the landing gear's overall dynamic behavior. This lack of physical detail is typical in current ADLs that target embedded real-time systems. Another example (from TELECOM ParisTech) is a flight controller for an F14 aircraft [17], which deals with mapping Simulink models into AADL components. A more comprehensive representation of the physical architecture of the aircraft would give designers the ability to easily map models for the aircraft dynamics (in multiple formalisms) into the corresponding physical components and connectors that describe the aircraft architecture. For example, the detailed Simulink/Modelica models for the aileron, flaps, and rudder could be associated with actuator components in the aircraft architecture. A similar mapping to physical domain components could be done for dynamic models of the sensors, the aircraft frame (mechanical), and engine system (fluid, thermal). This approach would help the design team to store the physical modeling information about the system from multiple tools along with component specifications from the cyber domain, in a single, unified framework. It would also give the system engineer the flexibility to explore design alternatives for the various avionic subsystems.

Another important consequence of incorporating the physical subsystems into the architecture is the ability to assess design trade-offs across the cyber-physical boundary. One could envision replacing a particular sensor with another having a better resolution/range, but with greater weight/cost. To study the systemwide effect of this change, one could analyse the performance to weight tradeoffs on the combined software and physical aircraft systems. Several relevant questions could be answered. For example, does the change impact the data rate of the communication channel between the high resolution sensor and the controller? Will the scheduling of the current task set still be valid with more information to process per sensor update cycle? Which would give better control performance: a better sensor with a simpler control algorithm or a less costly sensor with a memory-and processor-intensive controller? The answers to such questions involve choices in both the cyber and physical worlds, including the couplings between the two domains. Having a unified CPS architectural framework can decrease the lead-time to develop several ready-to-use architectures of the aircraft model, with different levels of detail, so that the engineers can investigate many more design alternatives with a high level of accuracy of the analysis, thus minimizing the risks of costly "design-build-test-fix" cycles.

A third benefit concerns the relationships between the multiple heterogeneous models utilized in the design and verification of a complex cyber-physical system. The exchange of information, assumptions, and inferences among the many groups of engineers involved is typically informal at best, and it is particularly difficult when the structure and semantics of the modeling formalisms differ significantly. Consequently, correctness of the design is inferred by a combination of engineering judgment supported by extensive testing of the final system. There is a need to develop an architectural formalism with structural and semantic annotations that can represent both cyber and physical system-level requirements and specifications along with the assumptions and implications associated with the many verification models developed for the system. The proposed CPS architectural style provides the reference context for making meaningful associations across the disparate models used for analysis and verification.

CPS Architectural Style

We use the Acme ADL [START_REF] Monroe | Foundations of Component-Based Systems, chapter ACME: Architectural Description of Component-Based Systems[END_REF], which has strong support for defining extensible architectural styles. In Acme, an architectural style is represented as a family of element types that adhere to rules governing what kind of components and connectors can be present in the system and the manner in which they can be connected. A general style can be refined into an application-specific style by extending existing types and adding additional element types and rules.

The challenge in defining an architectural style for cyber-physical systems is to strike a balance between specificity and generality. We focus on embedded monitoring and control systems. Our goal is to create a family of general components and connectors that can serve as the foundation for application-specific styles in this broad domain. Towards this end we define the following three related families pertaining to the cyber domain, the physical domain, and their interconnection. The goal of creating the CPS architectural style is to provide a representative set of components and connectors that can be extended to full implementations in targeted application frameworks.

Cyber family

The cyber side of CPS is the traditional domain for ADLs and provides support for standard real-time monitoring and control applications. The cyber components are: Data Stores: These components store data as an interface between the computational elements in the system. In simple systems, these could be just passive memory blocks. In complex systems there could be further details specifying what components can read and write to the data store components. Computation: Computation components operate on and update data posted in data store components. This includes components that perform filtering, state estimation, and control. IO Interfaces: These components perform the computations and timing functions required to sense and control the physical world. This would include, for example, smart sensor software that processes raw sensor data.

In addition to the computational aspects of the software, it is important to represent the communication elements in the system to reason about timing between software elements and how this affects the physical behavior of the complete system. We represent two major types of cyber connectors, a callreturn connector, representing one-to-one communication and a publish-subscribe connector for one-tomany communication.

The communication mechanism could be eventbased, synchronous or asynchronous, and is specified in the role defined for each connector. Furthermore, each connector type can be refined further, based on the communication semantics of the interacting components. For example, the publishsubscribe connector could be elaborated to define communication between CORBA components.

Physical family

There are several challenges in developing a suitable architectural representation of the physical side of cyber-physical systems. Architectural models should not have all the details required for a full simulation of the physical dynamics. At the same time, the architectural components and connectors should correspond to intuitive notions of physical dynamics in the same way cyber components and connectors correspond to elements of computational systems. To achieve this balance, we introduce components and connectors based on an energy view of physical systems. This provides a domain-independent perspective, including the ability to represent interactions between different physical domains and the possibility to specify system properties such as power flow and causality. This is similar to the perspectives taken in bond graphs [START_REF] Gawthorp | Bond Graphs and Dynamic Systems[END_REF] and Lagrangian mechanics [START_REF] Jeltsema | Multidomain modeling of nonlinear networks and systems[END_REF], where power-conjugated variables (effort and flow) describe signal flows between sources, energy storage elements, and dissipative elements.

The physical family is an architectural style to model multi-domain physical systems. When two or more components from the physical family are connected, the implication is that they exchange energy in some way. The ports of each physical component define its effort and flow variables. The product of this "power conjugate" pair equals generalized power in the physical domain of interest. Power flowing into a component is defined as positive. This is analogous to positive mechanical work being defined as work done by the applied force on the component. A component's constitutive equations (attached as behavior annotations) define the relationships between the port variables and the internal state variables. Each physical domain extends the basic port type by defining effort and flow variable types relevant to that domain, along with their units and ranges of acceptable values. For example, an electrical physical port would define voltage and current as the conjugate variables for electrical components. There would be two (or more) ports for each generic electrical component. The voltage across the component and the current through it (along with either charge or flux as the stored quantity) would be defined in terms of the conjugate variables at the electrical ports.

A connector (along with its roles) defines the relationship between the effort and flow pairs of all the components that are attached to the connector. The connectors constrain the form of energy exchange between the components by enforcing the laws of conservation of the respective physical quantities at all times. For example, an electrical connector's semantics would enforce Kirchhoff's current and voltage laws between the conjugate variables of its connected components.

The physical component types are: Energy sources: A source component delivers constant effort (or flow) to other components, regardless of the load presented to it. This is analogous to an ideal voltage (or current) source. Because of the defined direction of power, such components will have negative flow as long as they are supplying power to other components. A source behaves like an energy sink when it consumes power from its surroundings. An example is a rechargeable battery component in charging mode. Energy storage: An energy storage component models dynamic elements or subsystems that store energy, such as components that have capacitive and inductive properties in electrical systems. Ports on these components allow power transfer to other subsystems. Dissipative components: These model physical elements that lose energy over time. They correspond to resistors in electrical circuits and dampers or friction losses in mechanical systems. Power losses can take place in complex ways within physical components. Hence, the semantics of a dissipative component is completely defined by its energy loss function, which describes the relationship between the effort and flow variables of all its connected ports. Physical transducers: Transducers represent power transfer or energy conversion between different types of physical domains. These components are particularly useful in modeling multi-domain systems with, for example, electromechanical devices that transform energy between the electrical and mechanical domains. Transducers contain at least one port from each of the physical domains they interconnect.

The physical connector types are: Equal effort: The constraints on the power conjugate variables of the component ports coupled with this connector are: (1) the effort variables of all connected ports are equal; and (2) the sum of the flow variables of all connected ports is zero. This connector represents the application of Kirchoff's laws in the electrical domain and force/moment balance laws in the mechanical domain to coupled components. Equal variable: This connector indicates that the variables at the ports of the components are identical. There is no directionality associated with this connector. Measurement: Measurement connectors indicate conjugate variables that are determined by one physical component and used as an input in another physical component. Thus, these connectors are directional and correspond to connections in traditional block diagrams (e.g., signal lines in Simulink).

Cyber-physical interface family

We define the cyber-physical family to bridge between the cyber and the physical worlds. The following elements of the cyber-physical interface (CPI) family represent connections between computational and physical systems: CPI components: cyber-to-physical (C2P)/physical-tocyber (P2C) transducers; CPI connectors: cyber-to-physical/physical-to-cyber translators.

The difference between CPI components and CPI connectors is a matter of detail and sophistication in the interface. An intelligent sensor that performs signal processing functions might be represented as a CPI component, whereas a simple digital thermometer could be represented as a CPI connector.

Together, the three generic families can be combined to and extended to provide a unified model of a cyber-physical system. The generic CPS component and connector types can be used to define new families with application-specific features and attributes. For example, the physical family can be specialized to the translational/rotational mechanical domain by creating physical ports that define velocity/ angular velocity as effort variables and force/torque as flow variables. The source components become force/torque and velocity/angular velocity sources, respectively. Mass and moment of inertia (MI) correspond to energy storage elements. They represent the ability of a material body to store kinetic and potential energy. The energy storage concept can be generalized to a rigid body component, which contains both mass (annotated with the centre of gravity (CG) coordinates) and MI as subcomponents. The rigid body also contains body coordinate frames and transformations between them as annotated properties. Dissipative components reflect phenomena where mechanical energy is lost over time, such as static friction and viscous damping.

We can define three mechanical connectors, corresponding to the three physical connector base types. For example, an equal velocity connector defines a mechanical coupling between two or more components which constraints them to move with the same velocity in the given frame of reference, while the joint forces sum to zero. Equal variable connectors equate the force and velocities of the connected components, while measurement mechanical connectors can be used to interface force (torque) and velocity sensors to rigid body components.

Example: STARMAC Quadrotor

The Stanford Testbed of Autonomous Rotorcraft for Multi-Agent Control (STARMAC) [START_REF] Hoffman | Quadrotor Helicopter Trajectory Tracking Control[END_REF], a fleet of quadrotor helicopters, has been developed as a test bed for novel algorithms that enable autonomous operation of aerial vehicles. As shown in Figure 2, the vehicle has four rotors, arranged symmetrically about its body frame. The rotors are powered by lightweight, brushless DC motors, which result in a thrust of 8 N per rotor.

Figure 2. The STARMAC quadrotor [START_REF] Hoffman | Quadrotor Helicopter Trajectory Tracking Control[END_REF].

The hardware configuration of the STARMAC is shown in Figure 3. The vehicle is equipped with three separate sensors for full state estimation. A Microstrain 3DMG-X1 inertial measurement unit (IMU) provides three-axis attitude, attitude rate and acceleration, through a built-in estimation algorithm that relies on three gyroscopes, three accelerometers and three magnetometers. Height above the ground is determined using a sonic ranging sensor, either the Devantech SRF08 or the Senscomp Mini-AE with 3 to 5 cm accuracy. Three-dimensional position and velocity measurements are made using differential GPS relying on the Novatel Superstar II GPS unit. This unit outputs raw measurements at 10 Hz and the resulting position accuracy is 1 to 2 cm relative to a stationary base station. An onboard extended Kalman filter is used to combine GPS and raw inertial measurements for accurate full-state estimation. Computation and control are managed at two separate levels. The low-level attitude control, which performs real-time control loop execution and outputs PWM motor commands, occurs on a Robostix microcontroller based on the Atmega 128 processor. The high level planning, estimation and control occurs on either a lightweight Gumstix running embedded Linux on a PXA270 microprocessor, or on an Advanced Digital Logic ADL855 PC104 running Kubuntu Linux. Figure 3. Quadrotor hardware architecture [START_REF] Hoffman | Quadrotor Helicopter Trajectory Tracking Control[END_REF].

The Gumstix (0.05 kg) provides sufficient computational resources for carrier-phase differential GPS calculations and can be used to perform autonomous position control without the ability to add additional coordination algorithms between vehicles. As an alternative, the PC104 (0.48 kg) provides a wealth of computation power, at the cost of additional weight and hence, shortened flight times. The Robostix and Gumstix/PC104 communicate via a 115 kbaud RS-232 (serial) link. Communications between the highlevel computers and the ground station are managed through UDP over a WiFi network. The Gumstix uses 802.11b, and the PC104 uses 802.11g.

The ground station controller (GSC) is a high-level motion planner and coordinator for the quadrotor. It generates reference trajectories for the quadrotor to follow, displays telemetry data received from the vehicle, and manages coordination among multiple aircraft. The ground station also has joysticks for control-augmented manual flight, when desired. With reference to Figure 4, we see that the nonlinear dynamics of the quadrotor helicopter are those of a point mass m with moment of inertia

Quadrotor architecture in the CPS style

Figure 5 illustrates the use of the CPS style to model the quadrotor in AcmeStudio. On the cyber side, each controller (attitude, position, and GSC) is mapped to a separate computation component that implements the control algorithm. The communication of setpoints from a higher-layer controller to a lower-layer controller is modeled as a send-receive connector. The periodic relaying of vehicle state from the lower control layer to the higher layer is modeled as a publish-subscribe connector. This illustrates the use of distinct connector types to represent different communication patterns between the same components. Since there is no direct communication channel between the attitude controller and the ground station, no connector exists between them.

The vehicle frame is modelled as a rigid-body component, whose mass and MI are affected by the forces and moments acting at its ports, according to the dynamic equations of the quadrotor. The vehicle frame is annotated with the body and inertial reference frames along with the formations. Each rotor and motor actuator is modeled as a single electromechanical transducer called Act, containing an electrical port and two mechanical ports, one each for the translational and rotational domains. The component models the conversion of input motor voltage to an output thrust (force) and torque acting on VehicleFrame. As we refine the architecture, this composite component can have

) j j j j b v D j R I R j j b f j j j RB R F D e mge T R z M M M r T R z = = - + + - = + + × - ∑ ∑ 4 , 1 , ( ) ( ( )
sub-structure, where the motor and rotor are separate components, with a torque connector between them. Each Act is connected to the VehicleFrame by two equal velocity connectors, one for force balance and one for moment balance. This models the action and reaction phenomenon between each rotor assembly and the vehicle frame. The drag force is described as a dissipative component, whose magnitude depends on the wind velocity and the aircraft velocity, among other parameters.

The complex empirical relationship of drag force to the velocities at its ports is annotated as a behavior property of the component. Gravitational force is modeled as a flow source component, since it exerts a constant force on the airframe. It is connected to the vehicle frame by a measurement connector.

The IMU and GPS are both modeled as P2C transducers, since they perform filtering on their raw sensor readings. On the cyber side, they are connected to their respective controllers by publish-subscribe cyber connectors, since these sensors send periodic streams of data to the controllers. On the physical side, they are connected by measurement connectors to the vehicle frame. The sonar sensor is modeled as a simple P2C connector, going from the vehicle frame to the attitude controller. The connector is annotated with sonar parameters including detection beam width, effective range, and resolution. Each Act component is sent actuation commands from the attitude controller through C2P connectors, representing the conversion of cyber commands to voltage (PWM signals) for each motor.

Models as architectural views

In virtually all verification tools, models are constructed as collections of interacting components or modules. Thus, each verification model has a structure that can be viewed as an architecture with syntax and semantics defined by the particular formalism underlying the design of the tool. From a structural perspective, an architectural view supports the description of a derived architectural model to abstract over details that are irrelevant for a particular analysis. The relationships between components in the structure of a verification model and components in the CPS architecture will not generally be one-toone, however. Current tools do not provide insights into the relationships between architectural views. This represents a problem for architectural modeling, since it is generally impossible to understand how design decisions or analyses in one view impact those of another.

The approach proposed here focuses specifically on component-and-connector views representing the architectures of verification models as abstractions of a shared more-detailed baseline architecture. In this context, well-defined mappings between a view and the full architectural description can be used as the basis for identifying and managing the dependencies among the architectural views and to evaluate mutually constraining design choices. The full baseline architecture thus becomes the repository for retaining results from various analyses and designs so that the interdependencies are explicit. The rest of this section describes how an architect can represent two different models of the quadrotor system as distinct architectural views. The data flow view focuses on the control performance of the quadrotor and typically ignores controller implementation details such as scheduling of tasks and associated communication jitter and delays. In particular, it assumes lossless communication between the GSC and the position controller onboard the quadrotor. However, in the implemented system, the two controllers communicate via a lossy wireless network. To analyze how the quality of the communication channel affects the temporal assumptions of the controllers, the designer would have to create a detailed simulation of the network in Simulink model. However, this class of behaviors could be analyzed fairly easily in a process algebra perspective of the system, as shown in the following section.

Figure 6. Quadrotor Simulink model [START_REF] Hoffman | Quadrotor Helicopter Trajectory Tracking Control[END_REF].

Process algebra view

Finite State Processes (FSP) [START_REF] Magee | Concurrency: State Models and Java Programming[END_REF] is a process algebra in the tradition of CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], where behavior is modeled in terms of event patterns, called processes that denote sets of traces. Each event in a trace represents a discrete transition of a system. Patterns are built up out of operators that indicate the occurrences of events, sequencing of events, choice, and parallel composition. Parallel processes synchronize on shared events, which can also be used to pass values between processes. In general, FSP captures the behavior of cyber elements fairly well, while physical elements are described by abstracting away their continuous dynamics. The components in an FSP architectural view are those entities whose behavior can be described by an FSP primitive process. A connector between two FSP components signifies that the two processes interact with each other through events and describes the protocol for that interaction.

The FSP architecture view of the quadrotor currently abstracts over the dynamics of the quadrotor and focuses on the communication between the ground station and position controller components. The quadrotor system is a composition of the two FSP components in which the GSC sends a single position command to the PC after it gets a command from the user to move the Rotor to a location. The PC continuously provides position status information back to the GSC. It is assumed that the PC controls the rotor assembly reliably so that if it is told to move the rotor to a given position, it will do so. This is an assumption that would be verified with other moredetailed models of that part of the system, probably in a different modeling formalism. wireless UDP link while a lossy connector with retry might model a wireless TCP. The architecture can then be used to yield the complete FSP specification shown in Figure 7.

The property to be checked is the following: if the user tells the GSC to move the rotor to a particular position (abstracted as either position 0 or position 1), the GSC will eventually receive a status message from the PC that it is at that location. This FSP specification is analyzed by the Labelled Transition System Analyser [START_REF] Magee | Concurrency: State Models and Java Programming[END_REF] tool. The analysis tells us that the property holds when retrying connector is used, but fails when the lossy connector is used. This illustrates how a system designer might compare design tradeoffs in the cyber world between different protocols of interaction between GSC and PC.

Behavioural annotations and analyses

The architectural elements describe only the structural information about a system. To be able to do meaningful formal analysis on the system behavior, one must annotate the architecture with behavioral information. In Acme ADL, the behavioral annotation can be implemented via properties to capture the behavioral information. We have implemented the annotations for two types of behavioral modeling frameworks: FSP and Linear Hybrid Automata (LHA) [START_REF] Henzinger | The theory of hybrid automata[END_REF]. We have developed plug-ins as extension points of AcmeStudio, which will display only the relevant information pertaining to the element or system selected by the user. We have also built into the plugins the ability to generate analyzable text files from these properties. The plug-ins traverse the architecture, gather the relevant information distributed through out the structure and generate a text file that is analyzed by the relevant tool. Figure 8 shows a schematic of this analysis flow. Currently, there exists one plug-in for FSP that generates a file that can be analyzed by LTSA and another plug-in for LHA that generates a file that can be analyzed by Polyhedral Hybrid Automaton Verifier (PHAVer) [START_REF] Frehse | Proceedings of the fifth International workshop on hybrid systems: Computation and control (HSCC)[END_REF].

Because of the flexible development environment in AcmeStudio, a system designer can create a custom plugin for each of the formalisms used to model the system. Architectural elements are then annotated with properties relevant to each formalism. Figure 9 shows an LHA plugin being used to display annotations for each architectural element in an LHA view of a heating control system. The plugin framework is leveraged to generate analyses results from the heterogeneous behavioral annotations, and the results can be combined together or studied separately. Thus, the CPS architectural style along with these analysis tools provides a unifying framework to develop new methods for optimizing designs with re-spect to performance measures that characterize important features of the system behaviors.

Conclusion

This paper presents a presents a way to augment architectural descriptions with physical elements. The CPS architecture style provides a set of components and connectors for developing a complete architectural description of systems involving both cyber and physical elements. The CPS architecture becomes a frame of reference for multiple architectural views of a system corresponding to different modeling formalisms.

There are several directions for further research and development. In the current implementation, the architectural views are connected to the detailed CPS architecture through hierarchical Acme representations that identify the relationships between components and connectors in each view with the components and connectors in the CPS architecture. Acme does not currently support resolution of inter-view correspondences, however, so further work is needed both in theory and tool support to formalize and analyze issues of consistency and completeness of various architectural views. Currently, the analysis plugins rely on external analysis tools to present results. A key usability issue is to provide the results in the context of the architectural view from which they originated, and this is ongoing implementation work. Such tools would provide a unified context to explore design alternatives that cut across the boundaries that currently separate the methodologies that focus on either the cyber or physical elements of cyberphysical systems.

Figure 1 .

 1 Figure 1. AADL description of aircraft landing gear.

D

  is the aerodynamic drag force, and g is the acceleration due to gravity.

  from the plane of rotor j to the inertial coordinates and the body coordinates, respectively. One of our objectives is to formally represent such dynamic behavior in the CPS architecture for the quadrotor system.

Figure 4 .

 4 Figure 4. Quadrotor free body diagram [22].

Figure 5 .

 5 Figure 5. Quadrotor CPS architecture.

7. 1

 1 Data flow view From a control engineer's perspective, the quadrotor system can be viewed as a data flow (Simulink) model, as shown in Figure 6. The position and attitude controller components in this architectural view are represented by the robostix and gumstix subsystems in the Simulink model. The vehicle dynamics are represented by the starmac_dynamics block, and the GPS sensor is defined by the Superstar_II block. If each of these Simulink blocks could be mapped to a component type in a new 'data flow' architectural style, then the Simulink model could be thought of as an architecture instance in its own right. The component and connector semantics for this architectural style come from the underlying data flow semantics of the Simulink metamodel. With such a mapping defined, one can ask how the data flow architecture is related structurally and semantically to the underlying quadrotor CPS architecture.

Figure 7 .

 7 Figure 7. FSP specifications for quadrotor.

Figure 8 .

 8 Figure 8. Behavioral analysis using plugins.

Figure 9 .

 9 Figure 9. LHA annotations in AcmeStudio.

Acknowledgments

The authors thank F. Murray Fishbeck for his help with the development of the STARMAC example. This work was supported in part by National Science Foundation (NSF) under grant no. CNS0834701 and by U.S. Air Force Office of Scientific Research (AFOSR) under contract no. FA9550-06-1-0312.


Julien Delange

Laurent Pautet

Fabrice Kordon

Modeling and Validation of ARINC653 architectures

Keywords: AADL, ARINC653, validation, modelbased, Ocarina, REAL

A vionics systems must be carefully designed due to their criticality since fault may lead to loss of life. Thes e systems must be verified and certified. However, design of avionics arc hitectures becomes more and more complex due to an increasing demand of new functionalities. It makes very diffic ult to analyze systems and detect potential faults that may cause damages. This paper presents an approac h to model and validate avionics systems. Architecture requirements, properties and constraints are described with the Architecture Analysis and Design Language (AA DL) and its associated A RINC653 annex. Then, we apply validation rules to check system correctness and constraints enforcement. This approac h provides a high-level view of the system and eases the development of avionics system by validating their requirements at a modellevel, before any implement ation efforts

Introduction

Context Safety-critical systems have strong requirements to be enforced all over the development process. To prevent damages from occurring errors, safety-critical architectures are based on dedicated s ervices isolating soft ware components and enforcing safety requirements.

The A RINC653 standard addresses such issues and introduces the concept of partitioned architectures for the design of avionics software. The main purpose is to increase system reliability and dependability. To do so, ARINC653-compliant operating systems (OS) isolate software components in terms of space and time and provide fault detection/recovery mechanisms. They also provide configuration tables to associate recovery procedures with each pot ential fault that may occur at runtime.

Problem

We identify three problems in the design of ARINC653 architectures in terms of representation and analysis.

First, it is difficult to design A RINC653 architectures due to their amount of requirements and their associated services (communication, fault management, etc.). Since the ARINC653 standard does not provide an abstract repres entation of t he architecture, ARINC653 systems analysis and review are made by means of code analysis, which is tedious, error-prone and OS dependent.

Second, critical servic es of A RINC653 architectures and OS must be analyzed before implementation efforts. These services (hierarchical scheduler, fault recovering, etc.) must be automatically validated to ensure that specified requirements can be fulfilled.

Third, t he partitioning strategy must be verified to check that failure in a partition cannot affect another one. This is of particular interest since ARINC653 architectures can host components having different criticality levels. Thus, a fault that occurs in a component at a given criticality can impact other components at a higher criticality level. This behavior must be detected and avoided as soon as possible in the development process.

Proposed Approach

To overcome these problems, we propose to model and validate A RINC653 systems to check for safety requirements. To do so, we rely on a modeling language providing an appropriate semantics for safety-critical arc hitectures with isolation requirements. We need a modeling language that enables automation of verification efforts.

Among c urrently proposed languages, the Architecture A nalysis and Design Language (AADL) introduces a component-based approach t o describe both hardware and software as pects of the system. It defines several components that are aggregated by engineers to model t he system according to its requirements and properties.

This paper proposes an approach to model and validate A RINC653 systems with AADL. This new represent ation of this kind of architecture eases system analysis and validation.

We describe ARINC653 partitioned architectures with t heir time and space isolation concerns (hierarchical scheduling, partitions confinement in memory segments, etc.). Modeling patterns are based on the last version of the AA DL (version 2). It introduces new components relevant for the modeling of A RINC653 constraints. These patterns are being integrated in the AADL standard as an annex document (the ARINC653 annex ).

We also int roduce validation rules to enforce ARINC653 requirements in AA DL models. These rules check for isolation correctness (m emory, scheduling, and communications requirements) as well as potential impact bet ween components having different criticality levels.

We then show how these modeling patterns and associated verification rules c an help systems designers to develop safer systems. We also present the tools that support our modeling patterns and our verification rules.

Outline Section 2 presents the ARINC653 standard and the specific services and requirements of ARINC653 architectures and OS. Section 3 introduces the AA DL m odeling languages and describes our modeling patterns to model A RINC653 architectures.

Section 4 details ARINC653 requirements validation using AA DL models. It first presents our AADL-dedicated validation language, REAL, and details its use for A RINC653 sy stems validation. Finally, section 5 concludes and gives an overview of incoming work on this topic.

ARINC653

2.1. Overview of the standard ARINC653 [START_REF]Avionics Application Software Standard Interface[END_REF] is an industrial standard that defines a set of services for the design of safetycritical avionics systems. The main principle consists in partitioning applications according t o their criticality level. A partition is isolated in space and time and exec utes software components as if it was running on a dedicated processor.

Figure 1 -Overview of an ARINC653 system

Partitions are executed on top of a dedicated kernel/middleware: the ARINC653 module. The conceptual model behind A RINC653 is illustrated in figure 1. In this example, the system contains t wo partitions with different criticality levels: the one of partition 1 being higher than the one of partition 2. A connection bet ween the two partitions is supervis ed by the ARINC653 module to ensure that data sent by partition 1 is only received by partition 2.

The module handles both partitions time and space isolation. As a consequence, it manages address spaces (to store and isolate partitions code and data) and time slots (to execute partitions).

Time and space partitioning policies

ARINC653 isolates applications so a failure in a partition cannot affect other partitions that run on the same processor. This isolation is achieved through two partitioning policies: 1. Time partitioning: each partition is execut ed during a fixed and pre-defined time slice. The ARINC653 module schedules partitions using a cyclic algorithm repeated at a given period, called the major time frame. Typically, the value of the major time frame is equal to the sum of partitions time frames. At each major time frame, inter-partitions communication buffers are also flushed (dat a sent by one partition is available to its recipients). 2. Space partitioning: each partition owns a dedicated address space for its execution. In addition, inter-partitions communications are supervised by the module. This ensures that only allowed entities exchange data through a communication channel.

Services

The following subsections detail A RINC653 services.

Intra-partition communication services

Intra-partition communication services propose interfaces to enable communication between A RINC653 processes, located in the same partition. They do not use any module/kernel service and remain internal to the partition.

The standard defines four mechanisms: 1. Buffer stores multiple messages in message queues. Two queuing policies are propos ed (FIFO, Priority). 2. Blackboard stores one instance of a message until it is cleared or overwritten by a new instance. 3. Event is a notification service to indicate the completion of a job (wait/notify concept). 4. Semaphore service is used to control access to shared resources (e.g. counting semaphores).

Inter-partition communication services

Inter-partitions communication services propose functions to exchange data across partitions. They are supervised by the module, which ensure data transport. Communication policy (list of connected partitions ) is statically defined by the system designer so that partitions cannot create covert channels.

Inter-partitions communications are flus hed at each major time frame: data s ent by a partition is only received by its recipients during the next scheduling period. This behavior ensures communication determinism and eas es buffers dimensioning.

The standard defines the following inter-partition communication functionalities: 1. Queuing ports store multiple messages in queues. This service behaves like the buffer service. 2. Sampling ports carry successive updat ed messages of the same type. They are similar to the blackboard.

Health Monitoring service

The health-monitor service defines mechanisms to catch potential errors at run-time. E rrors can be caught at different levels (module/kernel, partition, process/task), depending on their nature (scheduling, exec ution error, etc.) and t he component they are issued from (module, partition or process). For eac h potential error, the system designer specifies an appropriate rec overing policy (for example, restart or stop the faulty component) in order to keep the system stable. He can also provide a dedicat ed recovery procedure.

ARINC653 systems constraints

Due t o their partitioning policy, ARINC653 systems have strong requirements that must be validated: Time isolation policy must guarantee that:

1. Each partition is scheduled at least one time during each scheduling period. 2. The value of the major time frame is consistent with partitions time frames. Space partitioning policy must allocate a distinct memory segment for each partition. Healt h Monitoring (HM) policy must ensure that all potential faults are bound to a recovery policy. Designers must ensure that each level of t he layered architecture (module, partition, process) uses a recovering policy for each potential fault. Such a validation is difficult to achieve hrough code review since it requires a good knowledge of the ARINC653 operating system internals. In addition, it is of special interest to analyze ARINC653 architectures at a specification -level. It helps certification engineers by finding faults that are difficult to det ect, such as the impact bet ween partitions evaluated at different criticality levels. For example, a partition at a low criticality level could impact another evaluated at a higher criticality level through a communication channel. If a fault is rais ed in the first partition, it could stop sending data to the other. The absence of fresh data in the highestcritical partition could lead to an application error. As a consequenc e, the fault raised in the lowest-critical partition is propagated t o the highest one. For that reason, impacts of faults between partitions having different criticality levels must be analyzed. Components describe elements of the architecture. Subprograms model application code. Since it is not an architectural element, it is reduced to a referenc e to another external piec e of code. Threads model the active part of an application (such as POSIX threads). Processes model address spaces containing threads. Processors model micro-processors and a minimal operating system (mainly a scheduler). Virtual processors model a part of the proc essor and could be understood in different ways: part of the physical processor, virt ual machine, etc. Memories model hard disks, RAMs. Buses model networks, wires. Virtual buses are not formally a hardware component, they are bound to c onnections in order to describe their requirements. They can be used for several purpos es (modeling protocol stacks, security layers, etc.). Devices model sensors or actuators. Systems represent composite components that are build from hardware components, software components or a combination of the two. For example, a system may represent a board with multiple processors and memory chips.

Modelling

Components hierarc hy of an AADL model is composed of several components and subcomponents. The topmost component is an AADL system that cont ains processes, processors and ot her architecture components.

The interface specification of a component is called a type and provides features (e.g. communication ports). Components communicate one with another by connecting their features (t he connections section). Each component describes their internals: subcomponents, connections between these sub-c omponents, etc.

An implementation of a thread or a subprogram component can specify call sequences to other subprograms, thus describing the execution flows in the architecture. Since there c an be different implementations of a given component type, it is possible to select the actual components to be put into the architecture, without having to change t he other components, thus providing a c onvenient approach to application configuration.

AADL allows properties to be associated with AADL model elements. Properties are typed and represent name/ value pairs that represent components characteristics and constraints. Examples are the period and execution time of threads, the implement ation language of a subprogram, etc. The standard includes a predeclared set of properties and users can int roduce additional properties through property definition declarations. For int erested readers, an int roduction to the AADL can be found in [START_REF] Feiler | The Architecture Analysis and Design Language (AADL) : An Introduction[END_REF].

Other languages can be integrated in AADL models by means of annex libraries. These languages can be added on eac h component to describe other aspects. Some annex languages have been designed, such as the behavior annex [START_REF] Frana | The AADL Behavior Annex -Experiments and Roadmap[END_REF] or the error model annex [START_REF] Rugina | Software Dependability Modeling Using an Industry-Standard Architecture Description Language[END_REF]. It provides a convenient way to specify other aspects of t he system (fault propagation, behavior, etc).

AADL provides two major benefits for building safety-critical systems. First, compared to other modeling languages, AADL defines low-level abstractions i ncluding hardware descriptions. Second, the hybrid system components help refining the architecture as they can be detailed lat er on during the design process.

ARINC653 modeling patterns

This section presents patterns we designed for the modeling of ARINC653 [START_REF]Avionics Application Software Standard Interface[END_REF] architectures. It follows the same organization as section 2.3. This work is also included in the A RINC653 annex document of the AADL, proposed for standardization by SAE.

Mapping partitions

An ARINC653 module (see section 2.1) is represented in AA DL by means of a processor component. It models the underlying A RINC653 module that provides time and space isolation. It contains partitions runtime as subcomponents and defines isolation requirements with AADL properties. Partitions are specified with two AADL components: 1. A virtual processor for the modeling of runtime c oncerns (tasks scheduling, partition resources, etc). 2. A process that describes the content of the partition (thread, data, etc).

The association between thes e components is defined with the Actual_Processor_Binding AADL property. The virtual processor is contained in a processor to model its containment in its related module. Space isolation (memory segments allocation) is specified by associating the process to a memory component with the AADL property Actual_Memory_Binding. Memory components describe segment requirements (size, etc).

Mapping ARINC653 processes

AADL threads model ARINC653 processes bec ause they share the same concept: an instruction flow constrained by some requirements (period, deadline, execution time and so ondescribed with AA DL properties). A RINC653 processes are contained in a partition so that AADL threads are contained in an AADL process.

Inter and intra-partition communications are mapped in AADL by connecting c omponents ports. When t wo connected threads belong to t he same process, the connection models an int ra-partition service. When they belong to distinct process components, it represents an inter-partition communication channel.

Mapping intra-partition communication

An ARINC653 buffer is represented with a connection of AA DL event data ports bet ween AADL thread components.

Modeling of A RINC653 blackboards is made with the connection of AADL data ports bet ween several AA DL threads. AADL data ports do not queue data; and thus, are semantically equivalent to the concept of ARINC653 blackboards.

ARINC653 events are described using AADL event ports between several AADL thread components. AADL event ports queue signals without any data. Thus, this concept is the same as the ARINC653 events.

The ARINC653 semaphore mechanism is represented using a shared AADL data component between several AA DL threads. The concurrency characteristic of the semaphore is specified using the Concurrency_Control_Protocol property.

Mapping inter-partition communication

An ARINC653 queuing port is represented by connecting AADL event data ports bet ween several AADL process components. AADL event data ports queue incoming data with respect to a given queuing policy, which corresponds to the concept of ARINC653 queuing ports.

The modeling of ARINC653 sampling port service is achieved wit h the connection of AA DL data ports between several AADL process components. AADL data ports do not queue data and thus, are semantically similar to A RINC653 sampling ports.

AADL properties are associated to ports to specify their characteristics (queuing policy, etc.).

Health monit oring mapping

The Health Monitoring service detects faults at different levels (module, partition, process) and executes a recovering procedure for each one. For its description with AA DL, we int roduce a property to represent faults (ARINC653::HM_Errors) and associate it with anot her property that models recovering procedures (ARINC653::HM_Actions). Both properties are associated to a component (processor, virtual processor or thread) that models a layer of the ARINC653 architecture (respectively module, partition or process).

Example

The modeling of an A RINC653 system with AADL is illustrated in figure 2. Two partitions (isolated in a memory segment) are execut ed on top of an ARINC653 module. One partition sends data to the other (an inter-partition channel).

The A RINC653 module is depicted with the AADL processor (arincmodule) and contains two virtual processor components (part1_rt and part2_rt) that represent partitions execution environment. Partitions content is specified using an AADL process, each partition having its own (prs_sender for the first partition, prs_receiver for the second).

An AADL component (main) models the organization of the memory with its segments (AA DL memory sub-components). Partition address spaces (AADL process components) are then associated with them to specify the space isolation policy.

Each partition (AADL process) contains one task (an AADL thread component ). We introduce an inter-partition communication channel between the partitions to model an int er-partition communication channel.

Partitions are connected using AADL data ports. According to our modeling patterns, this communication mechanism is an ARINC653 sampling port.

ARINC653 architecture s validation

This section shows how we use a constraint language to enforce in critical systems: time isolation, fault coverage and assessment of the all the fault-recovery strategy.

Introduction to REAL

REAL [START_REF] Gilles | Validating requirements at model-level[END_REF] (Requirements Enforcement Analysis Language) is a constraint-based language for AA DL. It aims at checking c onstraints on architectural descriptions at the specification step, saving significant time over verification at execution time.

REAL conc ept is similar to formal methods such as B [START_REF]The B-Book : Assigning Programs to Meanings[END_REF] by checking requirements on a set of elements using a dedicated language. It allows one to build sets whose elements are AADL entities (connections, components or subprogram calls). Verification can then be performed on either a set or its elements by stating Boolean expressions. The basic unit of REAL is a theorem. A theorem verifies an expression over all the elements of a set that is called the range set.

In order to write c omplex expressions, one can use predefined sets, which contain the instances of t he AA DL model of a given type, or build intermediary sets, using relations bet ween elements of sets (e.g. returns the elements of the set A which are subc omponents of any elements of the set B).

Finally, subtheorems calls can be used to build loc al or global variables, or to check prerequired constraints on the model. Callee theorems inherit at run-time from the caller environment (t he local_set), and the user can pass parameters. Thus, it is possible to design a library of theorems that will be used by higher-level, user-defined theorems. Such work has been done for schedulability analysis, response-time analysis and soft ware-hardware adequacy.

A basic example of a REAL theorem is illustrated in listing 1. This theorem checks that all processor components contained in the model have at least one virtual proc essor. On the model in figure 2, this theorem is verified: the main processor (arincmodule) contains two virtual processors (part1_rt and part2_rt). Then, this theorem checks that:

The receiver is classified at the lower criticality level if the fault-recovery policy of the sender generates transient data omission. The fault-recovery policy of the sender may not lead to transient omission. Theorem 8 follows the same validation pattern looks for permanent errors. Compared to theorem 7, the values of the allowed_actions variable contain recovery actions that imply a permanent data omission.

Conclusion

This paper presents an approach for the modeling and validation of ARINC653 architectures.

To do so, we first introduce modeling patterns to represent ARINC653 systems and their characteristics using the AADL modeling language.

Figure 2 -

 2 Figure 2 -ARINC653 example with AADL

theorem

  Processor_Contains_Partitions_Runtime foreach cpu in Processor_Set do vps := {x in Virtual_Processor_Set | Is_Subcomponent_Of (x, cpu)}; check (Cardinal (vps) > 0); end Processor_Contains_Partitions_Runtime; Listing 1 -REAL theorem example actions (in src_actions) that are used when a fault is raised in the source partition (spart).

We then define, thanks to the REAL language, a set of theorems that check dedicated properties on the AADL model. This verification rules allow engineers to check for a set of predefined rules ensuring stateof-the-art correctness properties.

Altogether, these two cont ributions set up an automat able approach to ensure a good design of safety-critical systems with regards to safety properties. Such an approach is a particular interest for avionics systems that rely on partitioned architectures and have to fulfill strong c ertification requirements. It helps AADL models to be processed by certification tools to system design prior to implementation by means of code generation.

Next sections present theorems to verify ARINC653 constraints (c.f section 2.4) using AA DL models.

Time isolation

Time isolation is enforced by validating that: 1. Each partition contained in an A RINC653 module is execut ed at least one time during each scheduling period. 2. The consistency of the major time frame according to partitions time frames.

The first theorem (listing 2) checks that each processor component (ARINC653 module) references at least one time each contained virtual processor (ARINC653 partition) in its allocated time frames (AADL property ARINC653::Slots_Allocation). Its validation ensures that each partition is executed at least one time during each period.

Listing 2 -Theorem for partition execution enforcement

The second theorem (listing 3) checks that the major time frame of each AADL processor component (A RINC653 module) is equal to the sum of partitions time frames (property ARINC653:: Partitions_Slots).

This ensures that the scheduling period is consistent with partitions time frames (see section 2.2 for a description of the requirements of the major time frame).

Listing 4 -Theorem for the validation of space isolation

This theorem also checks model correctness, ensuring that system memory is divided into several s egments. It first retrieves the main memory component (mainmem) and analyzes its memory sub-components (in partmem) that represent memory segments.

By doing so, this theorem ensures that system designer divides the main memory into several memory segments dedicat ed to a partition. var errors := List ("Module_Config", "Module_Init", "Module_Scheduling", "Partition_Scheduling", "Partition_Config", "Partition_Handler", "Partition_Init", "Deadline_Miss", "Application_Error", "Numeric_Error", "Illegal_Request", "Stack_Overflow", "Memory_Violation", "Hardware_Fault", "Power_Fail");

var actual_errors := (property (CPU, "ARINC653::HM_Errors") + property (VP, "ARINC653::HM_Errors") + property (thr, "ARINC653::HM_Errors"));

Check (Is_In (errors, actual_errors) and Is_In (actual_errors, errors)); end Check_Error_Coverage; Listing 6 -Theorem for the validation of the fault coverage policy

Fault coverage

In A RINC653 architectures, errors m ay be raised at three different layers of the architecture (module, partition, process).

To check that all faults are recovered, we verify that al faults are handled during the execution of each A RINC653 process (AADL thread component). To do so, the associated theorem (listing 6) analyses each thread component (process level), its associated process and virtual processor components (partition level) and the processor that supports the partition (module level).

For each AA DL thread component (t hat represents an ARINC653 process), the theorem computes the list (in the actual_errors variable) of the errors recovered by the thread itself but also by its associated virtual processor (A RINC653 partition) and processor (ARINC653 module). Then, it compares this list to the one of all potential errors (variable errors) that may be raised in the architecture. Another validation theorem checks that a recovery procedure in a partition at a low criticality level could impact another partition at a higher level. When a fault is raised in a process, the recovery policy impacts its partition. These entities (processes of t he partition) stop sending or receiving data t o/from t he other partitions. This could be an issue if they are classified at a different criticality level.

To detect this issue, we distinguish two types of errors:

Transient errors are temporary and happen when the recovering policy of the sender restarts the process or its partition. In that case, data is not sent for a temporary period. It impacts receiver components for period but once t he recovering strategy is finalized, the system continues to operate as normal.

Permanent errors happen when the recovery policy stops the process or its partition. Data is no longer sent, which can potentially affect recipients, especially if they are classified at a high c riticality level. In that case, data will not be sent unless the task or its partition is restarted. They analyze eac h AADL process component (ARINC653 partitions) and its connected process (ARINC653 partitions that receive data from t he former partition). Then, it retrieves the list of recovery