Shravan Narayan

Deian Stefan

Rajesh Gupta
email: gupta@cs.ucsd.edu

Keywords: Formal verification, type and proof theory, program and model analysis, hybrid systems

We propose a type-driven approach to building verified safe and correct IoT applications. Today's IoT applications are plagued with bugs that can cause physical damage. This is largely because developers account for physical constraints using ad-hoc techniques. Accounting for such constrains in a more principled fashion demands reasoning about the composition of all the software and hardware components of the application. Our proposed framework takes a step in this direction by (1) using refinement types to make make physical constraints explicit and (2) imposing an event-driven programing discipline to simplify the reasoning of system-wide properties to that of an event queue. In taking this approach, our framework makes it possible for developers to build verified IoT application by making it a type error for code to violate physical constraints.

I. INTRODUCTION

Watches, appliances, cellphones, vehicles, grids, sensor networks, factories, supply chains: edge devices and systems of the Internet of Things (IoT) sense and actuate our living to bring it closer to the data-centers of an invading internet. Unfortunately, building IoT applications that are safe and secure is notoriously difficult. Though the popular media and some researchers have been quick to attribute fault to IoT developers being careless and not prioritizing safety and security [START_REF] Lamb | Why is IoT so insecure?[END_REF], this fault placement is misguided. IoT developers are assigned with the heroic task of building applications that not only interact with the physical world, but are distributed and run on heterogeneous devices. Worse yet, the low profitmargins of IoT leave little room for serious testing and none for formal verification.

Indeed, most IoT developers take existing off-the-shelf components (e.g., Bluetooth stacks and LCD drivers), and glue them together using general-purpose programming languages like C. Unfortunately, these languages and the frameworks and libraries on top of them do not account for physical constraints. This makes it easy for developers to misuse hardware components-and either leave or introduce undefined behavior that can lead to physical damage.

Consider, for example, controlling a peripheral such as a stepper motor using Arduino's general-purpose IO (GPIO) interface (Figure 1). Writing to the GPIO pins directly to control the stepper is error-prone; languages like C make it easy for a developer to inadvertently change the direction Partially supported by Nankai University and by the National Science Foun-dation of China, under grant 61672074 of the motor, for example, by writing to the wrong pin number. Unfortunately, higher-level interfaces that encapsulate the underlying hardware protocol (e.g., Johnny Five's stepper API [START_REF]Johnny five api -stepper[END_REF]) are also often unsafe. These high-level APIs allow developers to drive the motor too fast, which can cause the stepper motor to lose torque and behave unpredictably. This, in turn, makes it impossible for the software to keep track of the actual motor position-the very purpose of a stepper motor. But, even if individual components are implemented correctly, composing them can introduce new classes of bugs and make it difficult to verify the system-level safety and security guarantees. Consider, for example, Arduino's stepper motor library which exposes a safe API that internally blocks to avoid running the motor too fast [START_REF]Arduino reference -stepper[END_REF]. Though safe, this API does not compose well with other components. For example, an LCD display may need to be updated (e.g., to reflect the motor position) and a keyboard driver may need to handle user input (e.g., to stop the motor) concurrently, as the stepper motor is being driven. A blocking API is incompatible with this: we cannot, for instance, ensure that the display always reflects the state of the motor or that the motor can be stopped.

More generally, the guarantees of a component in isolation do not often translate to a larger system, when the component is composed with others. This is because components compete for resources such as memory and CPU time. For example, a stepper motor component implemented using Arduino's stepper library may operate correctly, i.e., it runs at a particular speed, in isolation, but in a larger system other blocking interfaces (e.g., the LCD driver) may break these guarantees and cause it to run slower. This may, in turn, violate the physical constraints of the hardware the motor itself is driving (e.g., the mount of a CNC milling machine).

In this paper, we propose to tackle the challenge of building correct IoT applications, and cyber-physical systems more broadly, by changing the programming model. In particular, we propose a type-driven approach that (1) makes physical and hardware constraints explicit (2) allows developers to specify and verify application-specific properties. By taking a type-driven approach we ensure that developers cannot write code that violates physical models and, for example, drive stepper motors too fast. At the same time, we can ensure that building large systems from smaller components preserves these guarantees and any properties specified by the developer (e.g., that the motor run at a particular speed). Our key insights, which we propose to implement in the F* programming language, are:

• We can encode physical constraints as refinement types on parameterized hardware APIs. Refinement types allow us to ensure safety with respect to a model of the underlying hardware, and by using specialized real number solvers such as dReal, to match hardware models with the underlying physics. • We can enforce system-wide properties (e.g., global invariants and component composition) by decomposing programs into a set of event-driven tasks. System-wide properties can then be expressed as temporal logic statements over events, and enforced using F*'s type system.

In the rest of the paper, we elaborate on these insights and describe our scalable, type-driven approach in detail (Section III). First, however, we describe the detail the underlying challenge of building an end-to-end correct cyber-physical system (Section II).

II. THE DIFFICULTY OF BUILDING IOT APPLICATIONS

To illustrate the challenges that arise when building IoT applications, we consider a simplified garage-door opener. Our garage-door opener is a simple CPS device that, on the press of a button, drives a stepper motor to open or close a garage door. We assume that motor needs eight clockwise rotations to open or close the door, in full. To give developers fine-grained control of position, steppermotors rotate in small increments. Figure 2 illustrates the fourphase motor that is at the heart of this application. This motor rotates 360°in four steps, i.e., 90°increments, by writing HIGH to each of the four control pins (and thus existing each of coil). To open the garage door, we can thus implement a function (onOpenButtonPress) that simply write to the four GPIO pins directly: Physical constraints. Unfortunately, this code is not safe: it attempts to activate the different motor coils too fast. The step motor is a physical device that has constraints on the maximum rate at which it can step. At low speeds, the current applied to the GPIO pin has enough time to overcome the resistance and inductance of the motor's coils. However, at higher speeds, the charge build up in the coils is insufficient to generate the required torque for the motor. This results in the motor operating incorrectly, potentially leaving the door in a unknown state.

The above code is unsafe-Arduino's digitalWrite API does not enforce sufficient delays when operating the step motor. Instead, IoT developers (e.g., the Arduino stepper motor library [START_REF]Arduino reference -stepper[END_REF]) account for this issue by inserting a delay after each step: This blocking approach, unfortunately, may affect the responsiveness of the application. But, this is not fundamentallanguages like JavaScript make it easy to do this in a nonblocking fashion [START_REF]Johnny five api -stepper[END_REF].

Worse, delays are not enough: not all operational rates are safe.

Step-motors have dead-zones and resonance frequencies that depend on their physical characteristics. Operating a stepmotor in such unsafe zones results in imprecisions when taking a step. We explain safe-zones, dead-zones, resonance zones and the differential equations that model this behavior in the next section. Here we simply remark that the stepper motor must operate at a particular frequency corresponding to a safe zone-this physical constraint must be enforced when using the GPIO interface.

In practice, IoT developers account for this by using known safe rates (which they often find by trial and error). Unfortunately, even using high-level peripheral APIs that account for known-safe rates as such is not sufficient to guarantee safety. The external load on the motor may "shift" the safe zone from the "safe" default-to ensure safety, a verified system must model the physics and not rely solely on safe defaults.

Composition. To scale to large system, physical constraints must be enforced system-wide, in the presence of composition. For example, we must ensure that any sequence of door-open and -close operations operate respect the physical constraints of the motor. IoT developers rely on testing to capture such edge cases. But given the low-margins of IoT, these devices do not typically undergo exhaustive testing and therefore often miss such edge cases [START_REF]Police ground drones after reports they fall out of the sky[END_REF].

Even if we assume that we can handle all edge-cases, we run into further difficulties whenever we add new components. Consider, for example, extending our garage door openers with a wireless remote controller. A natural, but naive, approach to incorporating such a controller is to to listen for commands and open or close the door accordingly:

void onRemoteCommand(DoorCommand cmd) { if (cmd == OPEN) { onOpenButtonPress(); } else if (cmd == CLOSED) { onCloseButtonPress(); } }
This code-and the wireless driver and packet parsing code it relies on-shares resources with the code that operates the motor. Unfortunately, this also means that the code can reintroduce the safety bugs from before: the motor code may not get enough CPU time to run the motor at a safe rate. To guarantee the safety and correctness of our IoT device, we need to guarantee global properties of our system, i.e., we need to ensure that the composition of components, even when non-interfering, preserves the guarantees of each component.

Outlook.

The simple example of a garage door opener demonstrates the challenges that IoT developers face when trying to build safe and correct applications: they must not only account for complex physical constraints when interfacing with a peripheral, but do so across the stack, in the presence of other software/hardware components. As we scale to larger cyber-physical systems, the need for programming languages and frameworks that make it easier to write safe and correct code is paramount. In the next section, we discuss a first step toward such a framework.

III. A FRAMEWORK FOR SAFE AND CORRECT IOT

We propose to develop an event-driven framework for writing safe, correct, and performant IoT applications. Our framework builds on the F* programming language [START_REF] Swamy | Dependent types and multi-monadic effects in f[END_REF]. First, we leverage F*'s tools for writing verified safe programs, including its effect tracking, refinement types, and memory safety checks. Second, we leverage F*'s Kremlin backend [START_REF] Protzenko | Verified low-level programming embedded in f[END_REF] to emit efficient C code that can run on bare-metal microcontrollers such as the Arduino uno.

In the rest of this section, we outline the high-level design principles underlying this framework. In particular, we show how refinement types and our event-driven design paradigm can be used to write safe and correct IoT applications from the start. We also present some details on how we can model hardware to reflect physical constraints accurately. Board Specifications. Our framework provides a minimalist Arduino library with safe primitives that respects specifications of the chosen microcontroller. Consider the digitalWrite API which writes a digital value to a particular GPIO pin. In the Arduino uno (amtel328p), pins 0 to 13 are analog pins, while pins 160 to 165 are digital pins. For safety, we must guarantee that we only write digital values to the appropriate pins. This guarantee, can be encoded using refinement types: Refinement types combine data types with boolean predicates. The type pin in the above code is a byte type (UInt8) with a predicate that states its value must lie between 0 and 13 or between 160 and 165. (The range check is performed at compile time with the help of a SMT solver and does not incur any runtime performance penalty.) As shown in Fig. 3, this can be used to ensure that the digitalWrite API only accepts parameters of type digitalPin-and, in turn, guarantee that the IoT developer cannot misuse the board by, for example, accidentally using digitalWrite to write to an analog pin. We note that the interface of our hardware platform is still preliminary. Nevertheless, in large CPS designs, such architecture models play a central role [START_REF] Nakajima | Cyber-physical system design from an architecture analysis viewpoint[END_REF]. We hence seek structured, categorized, hierarchical representations of such interfaces, in the spirit of [START_REF]Systems modeling language[END_REF], [START_REF] Feiler | An overview of the SAE architecture analysis & design language (AADL) standard: A basis for model-based architecture-driven embedded systems engineering[END_REF], and propose to incorporate such interfaces using F*'s functors and modules. In particular, we seek models which allow static verification of program execution against the hardware interface. These models would incorporate logical, timed, concurrent abstractions of the hardware behavior. Specifying and Enforcing Constraints. Refinement types also allow us to specify higher-level constraints on code. For example, we can ensure that the stepper motor function step provided by our framework can only be called at a safe rate globally. Specifically, we enforces a delay between calls to the step motor with the help of two events. The step API, when called, creates a new globally visible event Stepping. Once a sufficient amount of time has passed, the framework automatically creates a globally visible StepComplete event. Consider the signature of the step API provided by our framework 1 : The precondition of step (the requires clause above) enforces that the last event must be a StepComplete event, ensuring the stepper motor is not currently stepping. Calling step when this is not provable leads to a compile-time error. The postcondition of step (the ensures clause above) states that the Stepping event is generated by the step and that, at some point in the future, the StepComplete event is created. This allows us to guarantee any program that uses the step API cannot run the motor too fast, provided that the duration of step meets the expected ranges specified in the hardware and physical model interfaces (describe below). Note that the preconditions and postconditions of the step API can, in the software specification, be expressed as linear temporal logic (LTL) statements [START_REF] Pnueli | The temporal logic of programs[END_REF]. These LTL statements are specified as first order statements that apply to the sequence of all events generated by the system. To ensure no performance overhead at runtime, these LTL statements may be expressed as ghost computation-statements that exist at compile-time to help prove safety, but are not executed at run-time.

Our approach of enforcing LTL statements on the flow of events may be naturally used to prove system-wide properties. Consider the following statement:

not exists Stepping next Stepping
Applying this statement to the main function's post condition would provide a guarantee that the stepper motor never took a second step before the first step issues the StepComplete event, i.e., there is always adequate delay between each step in the entire application. Indeed the same mechanism can be used to prove additional properties about the entire system. For example, in our garage-door opener, we can state that pressing the open button on the remote always results in the opening of the garage door: exists (OpenButtonPress eventually GarageDoorOpen) → Composition. Our framework provides a single threaded cooperative scheduler that runs the IoT application's tasks. Each 1 We elide some of the syntax to simplify exposition task runs uninterrupted, to completion. This ensures that the developer is not forced to reason about concurrency. To ensure multiple components' tasks may be modularly composed, our framework ensures that all tasks are finite in size. This ensures that no component can run a long or infinite task that uses all the CPU time. For example, we can ensure that the code that handles wireless remote commands cannot interfere with the stepper motor code and thus cause the motor to operate outside the safe zone. Internally, we rely on refinement types and a tick monad to restrict the size of tasks to a fixed number of CPU operations. Attempting to run a task larger than the maximum allowed task size would raise a compile-time error. The maximum task size is specified by the IoT developer and is checked against the timing constraints exposed from the hardware interface and the physical model. Modeling Peripherals. Our framework requires an accurate model of hardware along with specifications of safe values for hardware parameters (such as the maximum step rate of a stepper motor). To ensure safe operation of hardware, the framework specifies "safe zones"-values of hardware parameters that are safe along with proofs of their safety. The APIs exposed by our framework always enforce these models to ensure that IoT applications operate the hardware safely.

Consider the modeling of a stepper motor controller. The motor controller must certify the maximum step rate I, and precisely take it into account the timed semantics as a refinement type in the controller model. The first step in this process is to use existing models of stepper motors such as those available in Matlab (shown in Fig. 4). These models allow us to isolate the time interval below which a coil cannot charge up to 63% before phasing off. Next, we encode I(t) The 63% induction threshold suggested in [START_REF]What is stepper motor resonance?[END_REF] is reached at the maximal frequency of 10hz (solved using the L A T E X package tikz).

in the refinement types of hardware APIs exposed by our framework. I(t) is specified as a real valued ghost variable on the parameters of hardware APIs. This ghost variable generates real value constraints whose solution would indicate safety of the specified step rate. We submit the resulting constraints to dReal [START_REF] Kong | dreach: δ-reachability analysis for hybrid systems[END_REF] as shown in Fig. 5, to verify that the equations are δ-decidable for the step frequency interval F of the chosen platform. While the solution of Fig. 4 can be specified by simple SAT-modulo real constraints and solved using dReal, the proof that the motor actually stalls when the step frequency cross the boundary of I would require a more elaborate electromechanical model of the motor. Such models can be build in Matlab, dReal, HCSP [START_REF] Zhao | A "hybrid" approach for synthesizing optimal controllers of hybrid systems: A case study of the oil pump industrial example[END_REF], or differential dynamic logic (ddL) [START_REF] Platzer | The structure of differential invariants and differential cut elimination[END_REF] and the proof of their differential invariants using theorem provers like Isabelle and KeymaeraX [START_REF] Platzer | Keymaera: A hybrid theorem prover for hybrid systems (system description)[END_REF].

To compose such models and their invariants as contracts, we rely on approaches such as those of [START_REF] Lunel | Compositional proofs in differential dynamic logic dl[END_REF], which give a method for composing models in ddL using differential invariants. Fig. 6 shows hows the approach of [START_REF] Lunel | Compositional proofs in differential dynamic logic dl[END_REF] is applied to the model of a controlled tank in an automated factory. Specifically, this approach can be used to mechanically prove invariants of individual components expressed by hybrid ddL specifications (e.g., the tank's analog water-level gauge and the tank's digital controller) and then automate the construction and proof of the combined invariants with respect to the composed system-the controlled tank. Variability: So far, we have outlined a method for building verified IoT applications that takes into account formalized specifications of the hardware and physical environment. We outlined the some of the required artifacts, which consider a mathematically perfect model of time as temporal logic (software), real-time logic (hardware) and differential logic (physics). This, unfortunately, is unsatisfactory: every IoT device (e.g., the Arduino) is subject to errors and, more generally, variability [START_REF] Van Rantwijk | Arduino clock frequency accuracy[END_REF].

One expensive solution is to fix the underlying (Arduino) platform with additional hardware: a real-time clock or highprecision timers [START_REF] Edwards | The case for the precision timed (PRET) machine[END_REF] which will be used by the software model (e.g., delay function in our exmpl). An alternative approach is to develop a stochastic model of variation between the builtin clock and a real-time clock to increase the accuracy of the clock. But clocks are not the only concern: hardware variability also entails the loss of precision of modern hardware due to increasingly small fabric. Nano-scale circuits become less reliable and more expensive to produce. They no longer behave like precisely chiseled machines with tight tolerances. Modern computing tends to ignore the variability in behavior of underlying system components from device to device, their wear and tear over time (MTBF), or the environment in which the computing system is placed. The NSF Variability Expedition (variability.org) envisions a computing world where system components, led by proactive software, routinely monitor, predict and adapt to the variability of manufactured systems.

IV. RELATED WORK AND DISCUSSION

High-precision stepper motors are used in a myriad of applications: hard drives, computer-assisted design, precision mechanics, laser and optical equipment, medical equipment, etc. In high value applications such as medicine, the stepper motors used are, fortunately, subject to very precise specification requirements (e.g., the R and L of a step motors). Even so, the use of hardware such as stepper motors poses challenges with scale. Cyber-physical systems found in transportation, factories, grids, usually contains thousands of such individual control loops which result in intertwined software, hardware, mechanics and physics models. There have been several works that attempt to address this problem. These works approach the problem either in terms of "correctness by construction"-focusing on composition, modularity and end-to-end correctness, or in terms of "deep specification'focusing on abstraction and accuracy of hardware modeling. We describe some of these below. Correctness by Construction. Concepts of interfaces and contracts have been used to address compositionality in system design [START_REF] Benveniste | Contracts for system design[END_REF], [START_REF] Alfaro | Interface automata[END_REF], [START_REF] Sangiovanni-Vincentelli | Taming dr. frankenstein: Contract-based design for cyber-physical systems[END_REF]. They are now used in many modeldriven engineering environments (e.g., Ptolemy [START_REF]The ptolemy project[END_REF], BIP [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF], AADL [START_REF] Feiler | An overview of the SAE architecture analysis & design language (AADL) standard: A basis for model-based architecture-driven embedded systems engineering[END_REF], and SysML [3]) to, for example, support interface and/or requirement verification (by model checking). Most of the methods initially developed to implement such processes faced quadratic complexity barriers resulting from a predominant reliance on specific models of automata [START_REF] Alfaro | Interface automata[END_REF], [START_REF] Raclet | A modal interface theory for component-based design[END_REF], and the lack of abstraction capability, reversibility and traceability. However, recent work such as real-time and scheduling contracts [START_REF] Benveniste | Contracts for system design[END_REF], [START_REF] Yu | The challenge of interoperability: model-based integration for automotive control software[END_REF] demonstrated the applicability of contract theory for reasoning on real-time constraints resulting from component analysis of software, hardware and control. Online scheduling and service contracts have also been considered in [START_REF]Whip: safe composition of micro-services[END_REF], [START_REF] Stierand | Real-time scheduling interfaces and contracts for the design of distributed em-bedded systems[END_REF]. These proved to scale to commercial automotive applications (e.g., patents US9459840B1 and US9477446B1) by relying on gradually coarser system-level abstractions of component behaviors, and by making verification problems amenable to ILP and SAT-solving. Additionally, architecture analysis based on contracts have been introduced to develop the use of such abstractions for causal reasoning across domains [START_REF] Le | Refinement-based synthesis of correct contract model decompositions[END_REF], [START_REF] Ruchkin | Contract-based integration of cyber-physical analyses[END_REF].

Despite significant progress made by the aforementioned efforts, system design today is still confounded by a whole host of conflicting methods and tools that make systems noncompositional at multiple levels from physical construction to reasoning and validation. The challenges here include handling the large variety and number of abstractions, scalability, as well as the dynamic nature of computational elements. Time topology makes reasoning even more complicated as one must now account for differing views of time including event/causality in computing systems. Quasi-synchrony for embedded system design [START_REF] Baudart | A synchronous approach to quasi-periodic systems[END_REF], [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF], [START_REF] Desai | Approximate synchrony: An abstraction for distributed almost-synchronous systems[END_REF], delay-and latencyinsensitivity for desynchronized circuits and systems [START_REF] Carloni | A methodology for correct-by-construction latency insensitive design[END_REF], [START_REF] Potop-Butucaru | From concurrent multi-clock programs to deterministic asynchronous implementations[END_REF], precision-time computation (PRET [START_REF] Edwards | The case for the precision timed (PRET) machine[END_REF]), Spanner's TrueTime [START_REF] Corbett | Spanner: Gogle's globally distributed database[END_REF], and Roseline's time service for cloud and grid infrastructures [START_REF] Dongare | Pulsar: A wireless propagation-aware clock synchronization platform[END_REF], have successfully established sound layered abstractions between noisy time measurements incurred by hardware variability and physical operating conditions, occasioning clocks drift and jitters, and system and software protocols to mitigate them and restore sound correspondences between logical software time, hardware real-time and physical hazards. In fact, both [START_REF] Benveniste | Contracts for system design[END_REF], [START_REF] Ruchkin | Contract-based integration of cyber-physical analyses[END_REF] illustrate, in different ways, the inter-dependence of application, hardware, and physical constraints at the core of system integration, and demonstrate the impossibility of resolving them under strict separation and without integrative models of time.

Deep Specification. The pioneering SeL4 project demonstrated the barrier of a quadratic growth of proof obligations (in the size of code) [START_REF] Klein | sel4: formal verification of an OS kernel[END_REF], a barrier which every framework now seeks to avoid. The NSF DeepSpec project co-designed the specification and proof of the CertiKOS hypervisor in Coq [START_REF] Gu | Certikos: An extensible architecture for building certified concurrent os kernels[END_REF]. It proved the applicability of deep specification and multi-layered abstraction in operating system design by building and proving an entire system stack in one heroic person-year. CertiKOS does not, however, state the cost to get composition of layered abstractions right, which is data of interest to system architects Such a methodology is fortunately common to abstract model checking: to define backtracking facilities to reverse or unwind a component's abstraction to a more concrete one [START_REF] Plassan | Vérification formelle concluante des propriétés des systèmes multi-horloges[END_REF], or contract-based design, should a component abstraction mismatch another it is to be composed with: causally locating the component to refine its interface [START_REF] Le | Refinement-based synthesis of correct contract model decompositions[END_REF].

End to End Verification. Boosted by full-scale verification projects such as miTLS [START_REF] Bhargavan | Proving the tls handshake secure (as it is)[END_REF], verified programming languages [START_REF] Rondon | Liquid types[END_REF], [START_REF] Swamy | Dependent types and multi-monadic effects in f[END_REF] have demonstrated the ability to provide the modularity, multi-layered abstraction and proof capabilities compatible with a deep level of specification for system integration. Refinement type provide scalable logical abstractions and efficient proof automation tactics to gradually and compositionally model, compose, abstract, refine and prove systems built from variables, functions and modules typed by logical propositions with the potential to describe layered functions, modules, components, systems. Refinement type theory provides an unprecedented opportunities to bridge gaps across engineering domains by developing integrative verification and synthesis methods without breaking modularity.

Framework Design. Our main challenge is to develop a verified design methodology for CPSs that spans across the fields of hardware, middle-ware, software, signal processing and control design, across logical, discrete, continuous models of time. This goal is inspired from, and similar to, type-safe unikernels built using MirageOS [START_REF] Madhavapeddy | Unikernels: Rise of the virtual library operating system[END_REF] by the instantiatiation of parameterized system library modules written in OCaml.

Fig. 1 .

 1 Fig. 1. Stepper motor controlled by an Arduino microcontroller.

Fig. 2 .

 2 Fig.2. A simple step motors with 4 steps. Writing a high bit to a pin, causes the motor's shaft (the box in the middle) to turn towards the pin.

/

  / Rotate the motor 8 times to open the door void onOpenButtonPress() { for(rotation = 0; rotation < 8; rotation++) for(step = 0; step < 4; step++) { activateCoil(step); delay(...); } }

private

  type pin = p:UInt8 { (p>=0 && p<=13) \/ (p>=160 && p<=165) } type digital_pin = p:pin {p >= 0 && p <= 13} type analog_pin = p:pin {p >= 160 && p <= 165}

→Fig. 3 .

 3 Fig. 3. Type refinements in the Arduino platform interface

→(

  h -> not exists Stepping after StepComplete) ensures fun h0 x h1 -> exists Stepping && future StepComplete) →

Fig. 4 .

 4 Fig.4. A formalization of the induction I(t) = (1 -e -Rt/L )V /R of a coil with resistance R = 10, voltage V = 5 and inductance L = 2. The 63% induction threshold suggested in[START_REF]What is stepper motor resonance?[END_REF] is reached at the maximal frequency of 10hz (solved using the L A T E X package tikz).

Fig. 5 .

 5 Fig. 5. Compilation of type refinement constraints into a dReal problem

Fig. 6 .

 6 Fig. 6. Automated composition of contract in ddL.

ACKNOWLEDGMENT

This work is partially supported by Inria associate-project Composite and by Inria's International Chair program.


Haolan Zhan
email: zhanhl@ios.ac.cn

Qianqian Lin
email: linqq@ios.ac.cn

Shuling Wang
email: wangsl@ios.ac.cn

Jean-Pierre Talpin
email: jean-pierre.talpin@inria.fr

Xiong Xu

Naijun Zhan

Unified Graphical Co-Modelling of Cyber-Physical Systems using AADL and Simulink/Stateflow

Keywords: AADL, Simulink/Stateflow, Co-simulation, Code generation, Analysis

The efficient design of safety-critical embedded systems involves, at least, the three modelling aspects common to all cyber-physical systems (CPSs): functionalities, physics and architectures. Existing modelling formalisms cannot provide strong support to take all of these three dimensions into account uniformly, e.g., AADL is a precise formalism for modelling architecture and prototyping hardware platforms, but it is weak for modelling physical and software behaviours and their interaction. By contrast, Simulink/Stateflow is strong for modelling physical and software behaviour and their interaction, but weak for modelling architecture and hardware platforms. To address this issue, we consider the combination of AADL and Simulink/Stateflow, two widely used graphical modelling formalisms for CPS design in industry. This combination provides a unified graphical co-modelling formalism supporting the design of CPSs from all three software, hardware and physics perspectives uniformly. This paper focuses on the required concepts to combine them together, and outlines how to verify and simulate a system model defined using the combined graphical views of its constituents, by considering the case study of an Isollete System.

Introduction

Cyber-physical systems (CPSs), networked embedded systems (IoT, sensor networks), exploit computing units to monitor and control physical processes via wired or wireless communication. CPSs are omnipresent, from high-speed train control systems, power and control grids, automated plants and factories, transportations, to ground, sea, air and space. Most CPSs are entrusted with mission-and safety-critical tasks. Therefore, the efficient and verified development of safe and reliable embedded systems is a priority mandated by many standards, yet a notoriously difficult and challenging research domain.

As to standards, model-based design (MBD) has become a predominant development approach in the embedded system industry. In the MBD methodology, the development of a system starts by a model, based on which extensive analysis and verification are conducted, so that errors can be identified and corrected as early as possible, and at best before the system is implemented or built. Subsequently, abstract system-level models are refined to semantically more concrete models and to source code, by model-transformation. The merits of MBD is hence to, at least, include the following folds:

-Complexity becomes tractable and controllable, thanks to system level abstraction.

-Errors can be identified and corrected at the very early stages of system design.

-Correctness and reliability can be guaranteed by proving the refinement process and all decomposed subsystems (components). -Developers can fully reuse existing components and/or systems, to improve development efficiency even more.

Unsurprisingly, available formalisms and environment for CPS design are numerous, e.g., hybrid automata, Hybrid CSP (HCSP), differential logic, Ptolemy, Metropolis, C2E2, etc. in academia; Simulink/Stateflow, Modelica, SCADE, Labview, etc., in industry; UML, SysML, MARTE and so on, for MBD. Because of the tight coupling of hardware, software, and physics in CPS design, one has to model a complex CPS from the perspectives of functionality (software), physicality (physical environment and hardware platform), and architecture uniformly, but unfortunately, most of existing modelling techniques do not support all of these three aspects well and uniformly.

For instance, the Architectural Analysis & Design Language (AADL) [START_REF] Feiler | Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language[END_REF] is an architectural-centric model-based language developed by SAE International. It features strong capabilities to describe the architecture of a system due to the pragmatic (and practice-inspired) effectiveness of combining software and hardware component models. Meanwhile, it also supports the formal description of discrete behaviour using its BLESS Annex. Thanks to its succinct syntax, effective functionality and facilitated extensibility (by annexes i.e. plugins), AADL has been widely exploited in various embedded system domains, e.g., avionics, automotive. However, the core of the AADL only supports for modelling embedded system hardware structures and abstraction of its relevant discrete behaviour relevant to verification. It does not support the description of the continuous physical processes to be controlled by the embedded system and its combination with software, although some attempts have been done [START_REF] Ahmad | Hybrid annex: An AADL extension for continuous behavior and cyber-physical interaction modeling[END_REF][START_REF] Larson | BLESS: Formal specification and verification of behaviors for embedded systems with software[END_REF].

By contrast, Simulink [START_REF]Simulink User's Guide[END_REF] is the de facto standard toolbox that has demonstrated strong capabilities for the model-based analysis and design of signal processing systems. It contains a large palette of functional blocks and supports their composition by continuous-time synchronous data-flow, as well as an intuitive graphical modelling language reminiscent of circuit diagrams. It is thus appealing to practitioners and engineers for whom it is designed for. Moreover, Stateflow [START_REF]Stateflow User's Guide[END_REF] is a toolbox adding facilities for modelling and simulating reactive systems by means of hierarchical statecharts, extending Simulink's scope to event-driven and hybrid forms of embedded control.

However, Simulink/Stateflow can hardly model system architectures and hardware platforms. To address this issue, we complement Simulink with AADL to provide a unified graphical modelling formalism to support all the three perspectives of CPS design uniformly. The overview of the combination is given in Fig. 1. Our basic idea to First, we translate Simulink/Stateflow diagrams into HCSP to obtain a formalisation of their port declarations [START_REF] Zou | Verifying Simulink diagrams via a hybrid Hoare logic prover[END_REF][START_REF] Zhan | Formal Verification of Simulink/Stateflow Diagrams[END_REF][START_REF] Zou | Formal verification of Simulink/Stateflow diagrams[END_REF]. Second, we use Daikon [START_REF] Ernst | The Daikon system for dynamic detection of likely invariants[END_REF], or invariant generation [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] or, possibly, compositional proof tactics [START_REF] Lunel | Compositional proofs in differential dynamic logic dL[END_REF] to associate type classifiers with formal contracts.

Simulation of the whole graphical model, defined by the combination of AADL and Simulink views, amounts to coordinating code generated by both AADL and Simulink model simulators through effective port communications. Verification of the combined models are performed by translation to HCSP [START_REF] Liu | A calculus for hybrid CSP[END_REF][START_REF] Zou | Verifying Simulink diagrams via a hybrid Hoare logic prover[END_REF][START_REF] Wang | An improved HHL prover: an interactive theorem prover for hybrid systems[END_REF][START_REF] Chen | MARS: A toolchain for modelling, analysis and verification of hybrid systems[END_REF].

Contribution. In this paper, we propose a unified graphical framework using AADL and Simulink to model, simulate and verify cyber-physical systems. This framework depicts a methodology to design and simulate CPSs in a unified graphical environment while supporting formal verification of its functional, physical and structural artifacts uniformly using HCSP. Our graphical framework consists of AADL, its BLESS Annex and Simulink/Stateflow. It is implemented by a simulation environment called AADL-Sim, which integrates a set of tools, including an automatic translator from AADL into C, and a simluation engine combining AADL and Simulink/Stateflow models. To demonstrate the above framework and tool, the case study of an Isolette System is provided.

Paper Organization. The rest of the paper is organized as follows. Sec. 2 provides an overview of AADL, Simulink/Stateflow, and the notion of design by contract. Sec. 3 presents the Isollete case study, which will be used as a running example throughout the paper. Sec. 4 depicts our combined framework composed of AADL and Simulink/Stateflow, especially how to compute the type classifiers and define the contracts for Simulink/Stateflow diagrams. Sec. 5 presents in detail how to implement the co-modelling and co-simulation in the unified framework. Sec. 6 gives the related work and Sec. 7 concludes this paper and discusses some future work.

Preliminaries

In this section, we first provide an overview of the AADL standard, by highlighting its structure and BLESS Annex, then introduce Simulink/Stateflow with most relevant features of it. Finally, we briefly introduce the notion of design by contract.

AADL

AADL provides means to specify both the application software and the execution hardware of an embedded system, and supports textual, graphical and XML Metadata Interchange (XMI) specification formats. Components with type and implementation classifiers are instantiated and connected together to structure the system architecture. The AADL core language constructs are categorised into application software, execution platform and composite components. A system component represents a composite entity containing software, execution platform and system components.

Components and Connections

The execution platform category represents computation and communication resources including processor, memory, bus and device components. A processor component represents the hardware and software responsible for scheduling and executing task threads. Properties can be assigned to a processor component to specify scheduling policies, high-level operating system services and communication protocols. A memory component is used to represent storage entities for data and code. A device component can model a physical entity in the external environment: a plant or the software simulation of the plant. It can also be used as an interactive component like sensor or actuator. A bus component represents the physical connections among execution platform components.

Application software category consists of process, data, subprogram, thread, and thread group components. A process component represents the protected address space, which is bound to a memory component. A data component can be used to abstract data type, local data or parameter of a subprogram. A subprogram models the executable code which is called, with parameters, by thread and other subprograms. Thread is the only schedulable component with execution semantics to model system execution behavior. A thread represents sequential flow of the execution and the associated semantic automation describes life cycle of the thread.

A component type declaration defines interface elements and may contain features. Features comprise data, event and event data ports to transmit and receive data, control, and data/control respectively. Port communication is typed and directional. An in port receives data/control and an out port sends data/control while an in out port can send and receive data/control. Communication is realized through connections between ports, parameters and access to shared data. BLESS Annex. The Behavior Language for Embedded System with Software (BLESS) is a standardised annex independent of the core AADL language. BLESS extends AADL with the ability of specifying behaviour of component interfaces, providing formal semantics for AADL behavioural descriptions and automatically generating verification conditions to be proven. BLESS models state machines using guards and actions to give precise specifications of discrete hardware/software behaviours. BLESS also introduces assert and invariant sections in AADL to specify assertions and predicates that behavioural models must satisfy.

We refer to AADL standard document AS5506-B [START_REF]SAE International Standards. Aarchitecture analysis & design language[END_REF] for further details.

Simulink/Stateflow

Simulink is an environment for model-based design of dynamical systems, and has become a de facto standard in the embedded systems industry. It provides an extensive library of pre-defined blocks for building and managing block diagrams, and also a rich set of fixed-step and variable-step solvers for simulating dynamical systems. It also provides features such as subsystems for building large systems in a hierarchical way.

Stateflow is a toolbox adding facilities for modelling and simulating reactive systems by means of hierarchical statecharts. It extends Simulink scope to event-driven and hybrid forms of embedded control.

A Simulink model contains a set of blocks, subsystems, and wires, where blocks and subsystems cooperate by dataflow through the connecting wires. An elementary block receives input signals and computes output signals according to user-defined parameters altering its functionality. One typical parameter is sample time, which defines how frequently the computation is performed. Blocks are classified into two types: continuous blocks with sample time 0, and discrete blocks with positive sample time. For continuous blocks, the continuous state changes over time continuously, e.g. the position or the speed of a moving car. It is usually represented by an ordinary differential equation (ODE). Simulink provides an amount of ODE solvers for solving ODEs based on the numerical integration methods.

Stateflow offers the modelling capabilities of statecharts for reactive systems. It can be defined as Simulink blocks, fed with Simulink inputs and producing Simulink outputs. A stateflow diagram is composed of transitions, states and junctions. Each transi-tion connects a source state to a destination state. It it is labelled with E[C]{cAct}/tAct, where E is an event, C is the condition, cAct the condition action, and tAct the transition action. The event E triggers the transition to take place, provided that the condition C is true. As soon as C evaluates to true, the action cAct will be executed immediately, while tAct will be left pending and put in a queue first, and will be executed until a valid transition path is completed. A state is labelled by three optional types of actions: entry action, during action, and exit action.

Stateflow supports to construct flow charts using connective junctions and transitions, which can be used between states to specify decision logics to form transition networks. The Stateflow states can be composed to form hierarchical diagrams: Or diagram, for which the states are mutually exclusive and only one state becomes active at a time, and And diagram, for which the states are parallel and all of them become active simultaneously.

Being based on a large palette of individually simple function blocks and their composition by continuous-time synchronous dataflow as well as the modelling capabilities of statecharts for reactive systems, Simulink/Stateflow offers an intuitive graphical modelling language of CPSs for practicing engineers. Ordinary users can quickly build the model's framework by connecting the corresponding graphical modules and defining interfaces. Therefore, it is convenient and efficient to design and analyse the components using Simulink/Stateflow for co-simulation.

Design by Contract

Design by contract (DbC) is an engineering methodology whereby system designers should define semantically founded, precise and verifiable interface specifications for hardware and software components. These specifications extend the ordinary notion of abstract data type with logical properties describing the pre-conditions, post-conditions and invariants of a software function or of a hardware block.

The term design-by-contract is due to Bertrand Meyer in connection with the definition of the Eiffel programming language and his book Object-Oriented Software Construction [START_REF] Meyer | Object-oriented Software Construction[END_REF]. It is rooted in Hoare logic, where the contract (A,G) of a program P naturally corresponds to the provable assertion C {A}P {G} in some logical context C. Contracts has been algebraically meta-theorized by Benveniste et al. [START_REF] Benveniste | Contracts for system design[END_REF], systematically applied to model-based design frameworks like BIP [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF].

Recently, [START_REF] Lunel | Compositional proofs in differential dynamic logic dL[END_REF] extended the reach of design-by-contract to the case of modularly verifying hybrid system models by the introduction of contracts in a compositional design methodology for Differential dynamical Logic (ddL) [START_REF] Platzer | Logical Foundations of Cyber-Physical Systems[END_REF]. In this context, and by contrast, the contract of a given model Γ [α]φ consists the evolution domain H of the specification α, as assumption, and differential invariant φ, as guarantee.

Isollete System: A Running Example

In this section, we introduce the Isolette System as a running example throughout the paper. Isolette is an infant incubator described by the Federal Aviation Administration (FAA) in the Requirement Engineering Management Handbook (REMH) [START_REF] Lempia | Requirements engineering management handbook[END_REF]. This example is concise enough to demonstrate, and also abundant enough to contain both discrete control behaviour and continuous plants, as a classical hybrid system [START_REF] Ahmad | Hybrid annex: An AADL extension for continuous behavior and cyber-physical interaction modeling[END_REF].

Isollete System

The isollete example has been widely used to explain detailed behaviour for AADLbased development and new annexes, such as the BLESS Annex and the Error Model Annex [START_REF] Delange | Architecture fault modeling with the AADL error-model annex[END_REF]. Fig. 3 depicts the AADL graphical model of the isollete system, including processor, bus, sensor, actuator, controller, and controlled process with internal threads.

The system is used to maintain the temperature of the isollete box, a physical environment, within a desired range that is beneficial to infant. To this end, the controller obtains the temperature inside the box through the sensor, then computes an appropriate command to control the temperature through the actuator to switch on (off) the heater combined with the isollete box. The continuous evolution of temperature depends on the current status of the actuator. If the heater is on, the temperature will increase, otherwise decrease. According to the specification in the Section A.5.1.3 of the REMH [START_REF] Lempia | Requirements engineering management handbook[END_REF], when the isolette is properly switched on, the temperature of the heater will change at a rate of no more than 1 • F per minute. Based on this specification, the temperature of the isollete box (denoted by c) and the temperature of the heater (denoted by q) are formally modelled by the ODEs (1) below. The constant 0.026 stands for the thermal conductivity. When the controller commands the actuator to switch the heater on, the rise in temperature q will result in c going up. In this specification, we assume that the room temperature outside the box to be constant at 73 • F, although its variations could also be modelled. The desired temperature inside the isollete box should be kept at a range between 97 • F and 100 • F.

   ċ = -0.026 • (c -q) q = 1 if heater is on q = -1 if heater is off (1)

Requirements

Referring to environmental assumptions provided in the REMH, the following safety should be satisfied.

-Safety: The temperature inside the isollete box should be kept in between 97 • F and 100 • F, i.e., 97

• F ≤ c ≤ 100 • F.
Moreover, considering the uncertainties from initial states, sensor errors, disturbance of dynamics, and numerical error caused by floating-point calculation, etc., it is required -Stability and Robustness: The inside temperature c will be finally steered towards the valid range after some time.

At this point, it is obviously hard to specify this physical model in using AADL and its annexes alone, notwithstanding its interaction with the digital controller, hence the question mark in Fig. 2 and the need for a complementary hybrid annex.

Combination of AADL and Simulink/Stateflow

The combination of AADL and Simulink/Stateflow aims at providing a unified graphical co-modelling formalism for CPSs, with which software, physical environment and execution hardware of a CPS can be modelled in a uniform framework.

General Framework

The Fig. 1 we already presented, describes the high-level architecture of the proposed unified graphical framework together with the connection among the three different physical, hardware and software layers. The architecture layer, described as AADL system composite components, specifies the types of hardware and software components, and (part of) their implementation (an abstraction of their actual implementation), as well as their composition. It usually consists of a central processor unit classifier with several subcomponent devices (like sensor, controller, and actuator etc.). Each of these classifiers has its own type and implementation. For software functionality and physical processes, the architecture layer usually needs their abstractions, i.e., the type classifiers of these software and physical components. The type classifier of a component declares the set of input and output ports, specifies the contract of its behaviour, that are accessible from outside. By contrast, the implementation classifier of a component binds its type classifier with a concrete implementation in the software and physical layers.

Our framework provides two methods to describe the type classifier of a given Simulink/Stateflow model. The first one is to derive a type classifier, which is satisfied by the Simulink/Stateflow diagram, directly from its behaviour, see Sec. 4.2; the other is to define a contract in the style of an assume/guarantee pair, and then prove the given Simulink/Stateflow diagram to satisfy this contract, see Sec. 4.3.

In the software layer, software components are defined by their functionality, which can be done using either AADL or Simulink/Stateflow. In AADL, the functionality is defined by processes, and in each process, one or more threads may exist to describe specific controlling behaviours. The BLESS Annex can further be employed to specify the behavior of the system precisely. In order to establish stable communication between different processes, port declaration must be well defined. The AADL implementation in this layer will be binding to the corresponding software and hardware components in the architecture layer.

In the physical layer, the continuous behaviour of physical processes is implemented as Simulink/Stateflow diagram. In order to integrate the Simulink/Stateflow diagrams for implementing software or physical processes into the architectural layer, we need to define a type classifier for each Simulink/Stateflow diagram so that it can be assembled with other abstract components to form the architecture of the whole system at the architecture layer. We will explain the details of this process in the rest of this section.

Example 1. Now we can build a complete graphical model of the Isollete system with the combination as shown in Fig. 3, in which the Simulink/Stateflow diagram is given as Fig. 4.

Simulation.

To simulate the graphical model with the combination of AADL and Simulink, we propose a cross-layer co-simulation framework, in which the hardware platform, control software, and physical dynamics in the designed CPS can be taken into account uniformly. We will explain the details of such specification in Sec. 5.

Verification. To further verify a graphical model given by the AADL-Simulink combination, we translate it into HCSP, which is an extension of CSP introducing differential equations to model the continuous evolution of the plant and three types of interrupts to model the interaction between continuous and discrete behaviours [START_REF] He | From CSP to hybrid systems[END_REF][START_REF] Zhou | A formal description of hybrid systems[END_REF]. The formal verification of HCSP can be done along the lines of our previous work [START_REF] Liu | A calculus for hybrid CSP[END_REF][START_REF] Zou | Verifying chinese train control system under a combined scenario by theorem proving[END_REF][START_REF] Wang | An improved HHL prover: an interactive theorem prover for hybrid systems[END_REF][START_REF] Chen | MARS: A toolchain for modelling, analysis and verification of hybrid systems[END_REF]. Moreover, the correctness of the translation can be strictly proved using higher-order UTP [START_REF] Chen | A two-way path between formal and informal design of embedded systems[END_REF], which extends the classic Unifying Theories of Programming (UTP) [START_REF] Hoare | Unifying theories of programming[END_REF] to hybrid systems by introducing higher-order quantifications and differential relations. The technical details of this part will be reported in a subsequent paper.

Computing Type Classifier for Simulink/Stateflow Diagram

As we explained above, when combining Simulink/Stateflow with AADL, we need to provide an abstraction for each Simulink/Stateflow diagram, i.e., its type classifier, so that it can be assembled with other components to form the whole system at the architecture layer, while the diagram itself will be used as the implementation classifier The port declaration declares a set of ports used to input and output data between the component and other ones. However, Simulink diagrams can be hierarchical, and hence its external ports can sometimes not be extracted directly. For example, consider the triggered subsystems in a Simulink diagram, they do not have any input and output ports, but are triggered by events. Therefore, we need to analyse the whole system in detail in order to obtain all external ports, particular, event ports. Moreover, this often gets worse when Stateflow models are additionally considered.

To address this problem, we exploit the tool Sim2HCSP, a component in our toolkit MARS [START_REF] Chen | MARS: A toolchain for modelling, analysis and verification of hybrid systems[END_REF], which can translate a Simulink/Stateflow diagram into a formal HCSP process. By applying Sim2HCSP, all external ports of a Simulink/Stateflow diagram can now be translated, and exposed, by a set of channels in the corresponding HCSP model, which is stored in a separate file. In the case of the Simulink diagram in Fig. 4, we can for instance obtain the following port declaration: abstract babybox features heatCommand: in data port; boxTemp: out data port; end babybox;

The reminder of the specification defines the contract of the component. It specifies the properties that should be satisfied by any execution of the component. In this paper, we adopt two approaches to generate the constraints for a given Simulink/Stateflow diagram. The first one uses Daikon [START_REF] Ernst | The Daikon system for dynamic detection of likely invariants[END_REF]. The basic idea is to simulate the given Simulink/Stateflow diagram, and then run Daikon to generate a candidate invariant which satisfies all simulation runs. The more simulations are performed the more refined the generated invariant becomes. For example, considering the Simulink diagram in Fig. 4, by applying Daikon, we can obtain the following type classifier: Alternatively, we can generate invariants directly from the Simulink/Stateflow diagram, or the translated HCSP process, by using technique of invariant generation for hybrid systems, e.g., [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]. Reconsider the Simulink diagram in Fig. 4, by using invariant generation, we can instead obtain the following type classifier: The efficiency of the first approach is much higher, but the generated invariant (approximation) can only be linear. Moreover, it may not become an actual invariant, even by conducting enough runs to refine it. By contrast, the second approach can generate more expressive and semantically correct invariants, but the efficiency is normally very low. How to improve the efficiency of invariant generation for hybrid systems is still a challenging problem.

Defining Type Classifier as Contracts

Our goal is to exploit the HCSP model provided by Sim2HCSP [START_REF] Chen | MARS: A toolchain for modelling, analysis and verification of hybrid systems[END_REF] to support modular, component-wise analysis and verification of system models combined from architectures described in AADL and hybrid systems in Simulink/Stateflow.

In the logical framework of HCSP, our model of contracts will naturally follow along the lines proposed by Lunel et al. for differential dynamic logic [START_REF] Lunel | Compositional proofs in differential dynamic logic dL[END_REF][START_REF] Lunel | Parallelism and modular proof in differential dynamic logic[END_REF]. In that context, the contract of a specification α is defined by a pair (A, G) of properties. A, the assumption, is a formula defining the evolution domain of α and G, the guarantee, is a formula stating its differential invariant.

In the Hybrid Hoare Logic for HCSP [START_REF] Liu | A calculus for hybrid CSP[END_REF][START_REF] Wang | An assume/guarantee based compositional calculus for hybrid CSP[END_REF], these concepts are provided by the domain B of derivatives ṡ = e&B and by pre-and postconditions, and history formulas HF, respectively.

It is hence tempting to adapt the composition theorem of [START_REF] Lunel | Compositional proofs in differential dynamic logic dL[END_REF] to the HCSP framework, as it provides a way to automate the proof of a system's contract, e.g.

(A 1 ∧ A 2 , G 1 ∧ G 2 ) from the (possibly tedious) proofs that its components C i=1,2 satisfy the differential invariant G i in the domain A i .
This theorem is obtained by obeying to the following associative-commutative definition of parallel composition of hybrid components [START_REF] Lunel | Compositional proofs in differential dynamic logic dL[END_REF]Def. 7]:

α ⊗ β = (disc α ∪ disc β ∪ (cont α ⊕ cont β )) *
which amounts to composing discrete components disc by using repetition and choice and continuous components cont by the union, noted ⊕, of there derivative equations.

[21, Th. 2] proves the following: assume proof trees Γ i [C i ]G i stating that the G i s are invariants of the components C i s in contexts Γ i , for all i = 1, 2. Next, assume that the definitions in the C i s do not interfere, nor with the guarantees of all other G j s (i = j):

∀i∀j = i, dv(C i ) ∩ dv(C j ) = ∅ ∧ dv(C i ) ∩ uv(G j ) = ∅
with dv(C) denoting the variables defined by a component and uv(G) the variables used or referenced in a guarantee G. Then, there always exists a derivation of Γ i=1,2 [⊗ i=1,2 C i ](∧ i=1,2 G i ), which the proof of the theorem mechanically constructs: an automated proof tactic.

This model of compositional contracts can be employed to implement Sangiovanni's "meet in the middle" design methodology as the mitigation of software, hardware and physics constraints from the viewpoint of the target system architecture. In the case of the isolette, for instance, it can be used to verify the safety requirement of the isollette in nominal mode, Sec. 3.2 (i.e. after an initialization period) by cross-validating the differential invariant of the physical model with the (adequate) operations of its controller on the sensors and actuators, all four expressed by separate logical contracts. A use case of this method with KeymaeraX, concerning the well-known controlled watertank problem, is given in Lunel's PhD Thesis [START_REF] Lunel | Parallelism and modular proof in differential dynamic logic[END_REF].

Co-Modelling and Co-Simulation

This section details the implementation of the unified framework introduced in Subsec. 4.1 for designing and analyzing CPSs. The design flow of the framework is shown in Fig. 5. It consists of three stages: co-modelling, model translation, and co-simulation.

In the co-modelling stage, designers can exploit the toolkit OSATE/AADL and Matlab/Simulink to model different parts of systems. Port definitions are required in each of the separate parts in order to establish the connection between AADL and Simulink/Stateflow models. Then, in the model translation stage, in order to integrate the two separate models and analyse them as a whole, we translate both the AADL and Simulink/Stateflow models into C code. On one hand, we developed a toolkit named AADL2C Translator, a novel code generation plugin to parse the AADL standard textual file and transfer it into C code. On the other hand, auto generation of C code from Matlab/Simulink models is done directly by using the Real Time Workshop(RTW) toolbox of Matlab. In the co-simulation stage, the translated C code from AADL and Simulink will be combined at first by performing integration and parameter configuration. After that, the testbench files are generated for the model code. The model code together with the testbench files will be compiled by a C compiler, with the co-simulation results produced. The co-simulation results provide a feedback for engineers to analyse and revise their original designs in the modelling stage. All three stages are introduced in detail in the subsequent subsections.

Co-Modelling in AADL and Simulink/Stateflow

AADL modelling

The OSATE platform provides two different design patterns for engineers to build AADL models: graphical models and textual code. To exploit the internal mechanism of AADL, we choose the textual form to build our system. With the BLESS Annex, AADL is also able to specify the discrete behaviour of components. AADL takes a top-down pattern to build a system: a system classifier is defined at the beginning, and then all its hardware and software subcomponents are declared in system implementation. For the Isollete example, the type classifier and implementation for the whole system shown in Fig . 3 The heatCPU element defines the central processor. The heatSW the central process for specifying the functionality of the sensor, the actuator and the controller. The babybox stands for the isollete box. In the connections section, the ports of heatSW and the ports of babybox are connected, for transferring the heat command (representing the off or on status of the controlled variable) and the box temperature respectively. The properties section stipulates a binding relationship between the software and hardware subcomponents. We can omit the details of it here. The behaviours of the sensor, actuator and the controller are implemented as threads in AADL. In particular, the model of the controller is defined as follows: In the implementation, the controller defines the functionality using the BLESS Annex: the controller receives the measured temperature of the isollete box from the sensor via the input port measuredTemp, computes a difference between the temperature and the threshold, and then sends it to the actuator via output port diff. The actuator will decide whether to turn on or turn off the heat depending on that value.

Simulink/Stateflow modelling We will use Simulink/Stateflow to model the continuous behaviour of the CPS under design. For the Isollete box, we need to model the continuous behaviour defined by the ODE (1). The Simulink diagram has been given in Fig. 4.

Combination of models After building the models separately in AADL and Simulink/Stateflow, we will combine them to form the whole system. Our approach is to define abstract components in AADL and connect each of them to the corresponding Simulink/Stateflow models. For each abstract component, the type classifier declares all the ports connecting AADL and Simulink/Stateflow models, and the constraints for the actual behaviour. The abstract AADL type classifier of the isollete box is given in Sec. 4.2. The compiler AADL2C Translator receives a source file as input and automatically generates the corresponding C code. According to the AADL grammar, a model is usually composed of several components, each with two parts: type declaration and implementation. The AADL2C Translator creates a struct object for each type declaration, e.g.. system, process, thread, etc., and defines a collection of properties of the corresponding type classifiers. The implementation classifier is translated into individual sub-functions, associated with relevant type classifiers and specific names. Especially, for thread implementation, two extra functions are specified for thread scheduling: create thread() and thread scheduling(). The create thread() function adds a thread to a thread queue for dispatch, while the thread scheduling() is designed to execute threads according to the scheduling protocol specified in the AADL model, e.g., Rate-Monotonic Scheduling (RMS), Highest Priority First (HPF), etc.

In order to implement the port communications between different components efficiently, an additional Global Port Data Management (GPDM) unit is introduced in the target C code. The GPDM will store all of the output ports as global variables, with names of the format componentType componentName outputPortName. In each simulation cycle, the values of these variables will be updated once.

Translating Simulink/Stateflow model Matlab provides an automatic code generation tool that helps to translate Simulink/Stateflow models into C code. It greatly improves the quality and efficiency of development and simulation. Here we briefly introduce the steps for generating C code files from Simulink/Stateflow models.

Before the translation, we simulate the Simulink/Stateflow models to be translated independently in Matlab, to guarantee that the models are executable. Then we use the Code Generation Tool provided in Matlab to generate C code. The model configuration process is carried out to set the Configuration Parameters, including the code generation method, the format of the generated model, etc. In detail, we need to configure the following three parts:

-Solver setting for the model solver. We set the solver's step size to be fixed length as RTW can only generate code from a fixed step model. Fixed-point solver provides a variety of algorithms including continuous methods and discrete methods. For the Isollete case study, we set the time step to be 0.1s. -Hardware implementation provisions. The hardware implementation option is to specify the target hardware specification including the manufacturer and type of the chip, the word length, byte order of the chip and so on. In our framework, we set them as default. Co-simulation requests a starting point of program execution so that we specify a main method as an interface to connect the C code generated from Simulink/Stateflow model with the C code interface generated from AADL model.

Co-simulation

Now all the different parts of the system, including hardware components, application softwares and physical processes modelled in AADL and Simulink/Stateflow, have been translated into C code separately. In the co-simulation stage, we need to integrated all the separate C code files by defining the communication between them. The communication of distributed parts is implemented through the GPDM block mentioned above, which can be regarded as a global data memory storing all the data interfaces (external in/out ports) information of each component, such as AADL thread components and Simulink/Stateflow models. Local variables inside components are not considered by the GPDM block.

After the C code files are integrated, the simulation of the whole system can be performed. During simulation, it is allowed to set some configuration parameters, such as the global simulation clocks and the periodical simulation clocks. Besides, engineers can also assign different values to system variables in different simulation situations.

Simulation results of Isollete For the Isollete case study, we will check whether it fulfils the requirements mentioned in Sec. 3.2 by simulation. We first translate the AADL and Simulink model of the Isollete to C code, then consider two cases by setting different initial values for the variables. In the first case, both the temperature inside isollete box and heat actuator are initially set as 73 • F, same as the general room temperature. In the second case, the initial temperature inside the isollete box is set as 115 • F (higher than the maximum safety temperature), and the temperature for the heat actuator is still set as 73 • F. For both of them, the simulation period is set to 0.1 s. Fig. 7(a) and Fig. 7(b) show the simulation results for the two cases respectively, where the blue solid curve and yellow dashed curve represent the trajectories for continuous variables c (for box temperature) and q (for heat temperature) respectively. The simulation results show that, under the control of heat actuator, the temperature inside the isollete box will finally reach a stable state, within the safety range between 97 • F and 100 • F. The requirement defined in Sec. 3.2 is satisfied. AADL provides the notion of annex to support extensions to its core language. The key standardized annexes include the Behaviour Annex (BA) which extends AADL with the ability of defining component behaviour via state machines, and BLESS Annex [START_REF] Larson | BLESS: Formal specification and verification of behaviors for embedded systems with software[END_REF], which improves the state transition formalism by introducing assertions for supporting contract-based specifications. The simulation and analysis of AADL models have also been explored a great deal. ADeS was one of the simulation tools with considering the environment in which the system evolves. AADL Inspector produced by Ellidiss company is a powerful software that encompasses various features including schedulability analysis and dynamic simulation. There have also been some work on translation of AADL to other languages for analysis and simulation, e.g. AADL to BIP [START_REF] Chkouri | Translating AADL into BIP -application to the verification of real-time systems[END_REF], AADL to Sync [START_REF] Jahier | Virtual execution of AADL models via a translation into synchronous programs[END_REF], AADL to Maude [START_REF] Ölveczky | Formal semantics and analysis of behavioral AADL models in real-time Maude[END_REF] and so on. However, most of them focus on the discrete-time behaviours.

There have been some work on the extension of AADL for hybrid systems.

[30] models hybrid systems with AADL based on networks of timed automata, and uses the model checker UPPAAL for property analysis. [START_REF] Qian | Hybrid AADL: A sublanguage extension to AADL[END_REF] discusses a sublanguage extension to AADL to describe continuous behaviour, but it has difficulty in modelling complex continuous behaviour expressed with differential equations. In [START_REF] Ahmad | Behavior modeling and verification of movement authority scenario of chinese train control system using aadl[END_REF], a Hybrid Annex is presented, which is much more expressive in its ability to specify hybrid systems, yet it lacks relevant tools for further simulation and analysis of the hybrid models.

Compared with the above mentioned work, our proposed AADLSim framework coalesces AADL with Simulink for modelling of both discrete and continuous behaviours, and the flexible interaction between them. Moreover, it also provides extensive support for the analysis and simulation of the combined models through translating them into the same target language.

Conclusion and Future work

In this paper, we propose an unified graphical co-modelling and co-simulation framework for the design of cyber-physical systems. This proposed framework combines AADL and Simulink/Stateflow with which the gap between discrete control and continuous plant can be filled. The combined models are translated into C code for further analysis by co-simulation. Throughout the paper, we clarify the main concepts of the framework, outline the specific co-simulation flow and the verification process of the combined models. An Isollete system case study is provided to illustrate the framework.

For future work, we will investigate the translation of the combination into HCSP, a formal modelling language encoding hybrid system dynamics by means of an extension of CSP. Formal verification of HCSP is supported by an interactive Hybrid Hoare Logic prover based on Isabelle/HOL. As a consequence, the combined AADL and Simulink/Stateflow models can be verified. To make sure that the generated HCSP model is correct, the consistency between observational behaviours of the models at AADL and Simulink/Stateflow, and HCSP must be guaranteed in a rigorous way. This question, however, is known to be difficult, due to the inherent complexity of hybrid systems. To solve this problem, we consider to define the semantics of all the separate models in UTP, to prove their consistency in a unified semantic framework.

Fig. 1 :

 1 Fig. 1: An overview of the combination of AADL and Simulink

Fig. 2 :

 2 Fig. 2: AADL graphical model of Isolette system

Fig. 3 :Fig. 4 :

 34 Fig. 3: AADL graphical model of Isolette system

  assert <<TIME: :(t >= 0.1)>> <<HEAT_T: : ((1.35107 * 10 ** 15) * t-(1.35107 * 10 ** 15) * q+9.862881 * 10 ** 16=0)>> <<H_VAR: : ((2.111 * 10 ** 13) * q-(2.111 * 10 ** 13) * orig(q)+1.056 * 10 ** 12=0)>> <<TEMP_VAR: : ((2.463 * 10 ** 11) * c-(2.744 * 10 ** 11) * orig(c)+2.055 * 10 ** 12=0)>> invariant <<TIME() and H_VAR() and H_VAR() and TEMP_VAR()>>

  assert<<L_LIMIT: : ((q-c) * e ** (-0.026 * t)+q * (c-97)<=0)>> <<H_LIMIT: : ((q-c) * e ** (-0.026 * t)+q * (100-c)>=0)>> invariant <<L_LIMIT() and H_LIMIT()>>

Fig. 5 :

 5 Fig. 5: Co-modelling and co-simulation of AADL and Simulink/Stateflow

5. 2

 2 Model Translation to C Translating the AADL model The translation from AADL to C is the most crucial part in the unified framework. It uses a collection of mapping rules from AADL concepts to C implemented by the compiler AADL2C Translator. Fig. 6 illustrates the model translation flow from AADL to C. AADL models can be defined in graphical or textual format: graphical models only describe the high-level architecture, while textual model includes the details such as the functional behaviours.

Fig. 6 :

 6 Fig. 6: An example illustrating the model translation flow from AADL to C

Fig. 7 :

 7 Fig. 7: Results of co-simulation from different inital stages

  are given as follows:

	system isollete
	end isollete;
	system implementation isollete.impl
	subcomponents
	heatCPU: processor heatCPU;
	heatSW: process heatSW.impl;
	babybox: abstract babybox.impl;
	connections
	cnx1: port heatSW.heatCommand -> babybox.heatCommand;
	cnx2: port babybox.boxTemp -> heatSW.boxTemp;
	properties
	......
	end isollete.impl;

-

  System object file of the model. The generated object files include a set of C source and header files. Suppose we call the Simulink/Stateflow model as box, the generated C files will include box.c, box data.c, box.h, box private.h and box types.h. The box.h and box.c define the main behaviour of the original model, while box data.c stores relevant constants or initial data, and the rest are the clarification header files.

Jean-Pierre Talpin is partially supported by Nankai University