{'fraction_non_alphanumeric': 0.034213861000097476, 'fraction_numerical': 0.005799785554147578, 'mean_word_length': 4.5075828747819084, 'pattern_counts': {'":': 0, '<': 16, '<?xml version=': 0, '>': 16, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude

Distributed cyber-physical systems (DCPS) are pervasive in areas such as aeronautics and ground transportation systems, including the case of distributed hybrid systems. DCPS design and verification is quite challenging because of asynchronous communication, network delays, and clock skews. Furthermore, their model checking verification typically becomes unfeasible due to the huge state space explosion caused by the system's concurrency. The PALS ("physically asynchronous, logically synchronous") methodology has been proposed to reduce the design and verification of a DCPS to the much simpler task of designing and verifying its underlying synchronous version. The original PALS methodology assumes a single logical period, but Multirate PALS extends it to deal with multirate DCPS in which components may operate with different logical periods. This paper shows how Multirate PALS can be applied to formally verify a nontrivial multirate DCPS. We use Real-Time Maude to formally specify a multirate distributed hybrid system consisting of an airplane maneuvered by a pilot who turns the airplane according to a specified angle through a distributed control system. Our formal analysis revealed that the original design was ineffective in achieving a smooth turning maneuver, and led to a redesign of the system that satisfies the desired correctness properties. This shows that the Multirate PALS methodology is not only effective for formal DCPS verification, but can also be used effectively in the DCPS design process, even before properties are verified.


Introduction
Distributed cyber-physical systems (DCPS) are pervasive in areas such as aeronautics, ground transportation systems, medical systems, and so on; they include, in particular, the case of distributed hybrid systems, whose continuous dynamics is governed by differential equations. DCPS design and verification is quite challenging, because to the usual complexity of a non-distributed CPS one has to add the additional complexities of asynchronous communication, network delays, and clock skews, which can easily lead a DCPS into inconsistent states. In particular, any hopes of applying model checking verification techniques in a direct manner to a DCPS look rather dim, due to the typically huge state space explosion caused by the system's concurrency.
For these reasons, we and other colleagues at UIUC and Rockwell-Collins Corporation have been developing the physically asynchronous but logically synchronous PALS methodology [9,11], which can drastically reduce the system complexity of a DCPS so as to make it amenable to model checking verification (for a comparison of PALS with related methodologies see [13]). The PALS methodology applies to the frequently occurring case of a DCPS whose implementation must be asynchronous due to physical constraints and for fault-tolerance reasons, but whose logical design requires that the system components should act together in a virtually synchronous way. For example, distributed control systems are typically of this nature. The key idea of PALS is to reduce the design and verification of a DCPS of this kind to the much simpler task 1 of designing and verifying the idealized synchronous system that should be realized in a distributed and asynchronous way. This is achieved by a model transformation E → A (E , Γ) that maps a synchronous design E to a distributed implementation A (E , Γ) which is correct-by construction and that, as shown in [9,10], is bisimilar to the synchronous system E . This bisimilarity is the essential feature allowing the desired, drastic reduction in system complexity and making model checking verification feasible: since bisimilar systems satisfy the exact same temporal logic properties, we can verify that the asynchronous system A (E , Γ) satisfies a temporal logic property ϕ (which typically would be impossible to model check directly on A (E , Γ)) by verifying the same property ϕ on the vastly simpler synchronous system E .
The original PALS methodology presented in [9,11] assumes a single logical period, during which all components of the DCPS must communicate with each other and transition to their next states. However, a DCPS such as a distributed control system may have components that, for physical reasons, must operate with different periods, even though those periods may all divide an overall longer period. That is, many such systems, although still having to be virtually synchronous for their correct behavior, are in fact multirate systems, with some components running at a faster rate than others. An interesting challenge is how to extend PALS to multirate DCPS. This challenge has been given two different answers. On the one hand, an engineering solution for Multirate PALS based on the AADL modeling language has been proposed by Al-Nayeem et al. in [1]. On the other hand, three of us have defined in [4] a mathematical model of a multirate synchronous system E , and have formally defined a model transformation that generalizes to multirate systems the original single-rate PALS transformation defined in [9,10]. As before, we have proved in [4] that MA (E , T, Γ) is a correct-by-construction implementation of E , and that E and MA (E , T, Γ) are bisimilar, making it possible to verify temporal logic properties about MA (E , T, Γ) on the much simpler system E .
But how effective is Multirate PALS in practice? Can it be applied to formally verify important properties of a nontrivial multirate CPS such as a distributed hybrid system? The main goal of this paper is to show that the answer is an emphatic yes. We use Real-Time Maude [12] to formally specify in detail a multirate distributed hybrid system consisting of an airplane maneuvered by a pilot, who turns the airplane according to a specified angle α through a distributed control system with effectors located in the airplane's wings and rudder. Our formal analysis revealed that the original design had control laws that were ineffective in achieving a smooth turning maneuver. This led to a redesign of the system with new control laws which, as verified in Real-Time Maude by model checking, satisfies the desired correctness properties. This shows that the Multirate PALS methodology is not only effective for formal DCPS verification, but, when used together with a tool like Real-Time Maude, can also be used effectively in the DCPS design process, even before properties are verified. To the best of our knowledge, this is the first time that the Multirate PALS methodology has been applied to the model checking verification of a DCPS. In this sense, this paper complements our companion paper [4], where the mathematical foundations of Multirate PALS were developed in detail, but where only a brief summary of some of the results presented here was given.
This paper is organized as follows. Section 2 explains Multirate PALS and Real-Time Maude. Section 3 describes a simple model of an airplane turning control system whose continuous dynamics is governed by differential equations. Section 4 presents a modeling framework for multirate ensembles in Real-Time Maude, and Section 5 then formally specifies the airplane turning control system using the ensemble framework. Section 6 illustrates Real-Time Maude-based verification of the airplane turning control system. Finally, Section 7 gives some concluding remarks.

Multirate PALS
In many distributed real-time systems, such as automotive and avionics systems, the system design is essentially a synchronous design that must be realized in a distributed setting. Both design and verification of such virtually synchronous distributed real-time systems is very hard because of asynchronous communication, network delays, clock skews, and because the state space explosion caused by the system's concurrency can make it unfeasible to apply model checking to verify required properties. The (single-rate) PALS ("physically asynchronous, logically synchronous") formal design pattern [9,11] reduces the design and verification of a virtually synchronous distributed real-time system to the much simpler task of designing and verifying its synchronous version, provided that the network infrastructure can guarantee bounds on the messaging delays and the skews of the local clocks.
We have recently developed Multirate PALS [4], which extends PALS to hierarchical multirate systems in which controllers with the same rate communicate with each other and with a number of faster components. As is common for hierarchical control systems [1], we assume that the period of the higherlevel controllers is a multiple of the period of each fast component. Given a multirate synchronous design E, bounds Γ on the network transmission times and clock skews, and function T assigning to each distributed component its period, Multirate PALS defines a transformation (E, T, Γ) → MA (E, T, Γ) mapping each synchronous design E to a specification MA (E, T, Γ) of the corresponding distributed multirate real-time system. In [4] we formalize Multirate PALS and show that the synchronous design E and the asynchronous distributed model MA (E, T, Γ) satisfy the same temporal logic properties.
Multirate Synchronous Models. In Multirate PALS, the synchronous design is formalized as the synchronous composition of a collection of typed machines, an environment, and a wiring diagram that connects the machines. A typed machine M is a tuple M = (D i , S, D o , δ M ), where D i = D i 1 × · · · × D i n is an input set, S is a set of states, D o = D o 1 × · · · × D o m is an output set, and δ M ⊆ (D i × S) × (S × D o ) is a transition relation. Such a machine M has n input ports and m output ports.
To compose a collection of machines with different rates into a synchronous system in which all components perform one transition in lock-step in each iteration of the system, we "slow down" the faster components so that all components run at the slow rate in the synchronous composition. A fast machine that is slowed, or decelerated, by a factor k performs k internal transitions in one synchronous step. Since the fast machine consumes an input and produces an output in each of these internal steps, the decelerated machine consumes (resp. produces) k-tuples of inputs (resp. outputs) in each synchronous step. A k-tuple output from the fast machine must therefore be adapted so that it can be read by the slow component. That is, the k-tuple must be transformed to a single value (e.g., the average of the k values, the last value, or any other function of the k values); this transformation is formalized as an input adaptor. Likewise, the single output from a slow component must be transformed to a k-tuple of inputs to the fast machine; this is also done by input adaptors which may, for example, transform an input d to a k-tuple (d, ⊥, . . . , ⊥) for some "don't care" value ⊥. Formally, an input adaptor α M for a typed machine ..,n} , each of which determines a desired value from an output D k of another typed machine.
Typed machines (with rate assignments and input adaptors) can be "wired together" into multirate machine ensembles as shown in Figure 1, where "local" fast environments are integrated with their corresponding fast machines. A multirate machine ensemble is a tuple where: (i) J S (resp., J F ) is a finite set of indices for controller components (resp., fast components), and e ∈ J S ∪ J F is the environment index, (ii) {M j } j∈J S ∪J F is a family of typed machines, (iii) the environment is a pair E = (D e i , D e o ), with D e i the environment's input set and D e o its output set, (iv) src is a function that assigns to each input port ( j, n) (input port n of machine j) its "source," such that there are no connections between fast machines, (v) rate is a function assigning to each fast machine a value denoting how many times faster the machine runs compared to the controller machines, and (vi) adaptor is a function that assigns an input adaptor to each l ∈ J F ∪ J S .  The transitions of all machines in an ensemble are performed simultaneously, where each fast machine with rate k performs k "internal transitions" in one synchronous transition step. If a machine has a feedback wire to itself and/or to another machine, then the output becomes an input at the next instant. The synchronous composition of a multirate ensemble E is therefore equivalent to a single machine M E , where each state of M E consists of the states of its subcomponents and of the contents in the feedback outputs, as explained in [4,10]. The synchronous composition of the ensemble in Figure 1 is the machine given by the outer box. Since M E is itself a typed machine which can appear as a component in another multirate ensemble, we can easily define hierarchical multirate systems.

Real-Time Maude
Real-Time Maude [12] extends the Maude language and tool [6] to support the formal modeling analysis of real-time systems in rewriting logic. In Real-Time Maude, the data types of the system are defined by a membership equational logic [6] theory (Σ, E) with Σ a signature 2 and E a set of confluent and terminating conditional equations; the system's instantaneous (i.e., zero-time) local transitions are defined by (possibly conditional) labeled instantaneous rewrite rules 3 ; and time elapse is modeled explicitly by tick rewrite rules of the form crl [l] : {u} => {v} in time τ if cond, which specifies a transition with duration τ from an instance of the term {u} to the corresponding instance of the term {v}.
The Real-Time Maude syntax is fairly intuitive. A function symbol f is declared with the syntax op f : s 1 . . . s n -> s, where s 1 . . . s n are the sorts of its arguments, and s is its (value) sort. Equations are written with syntax eq u = v, or ceq u = v if cond for conditional equations. We refer to [6] for more details on the syntax of Real-Time Maude.
A class declaration class C | att 1 : s 1 , . . . , att n : s n declares a class C with attributes att 1 to att n of sorts s 1 to s n . An object of class C is represented as a term < O : C | att 1 : val 1 , ..., att n : val n > where O is the object's identifier, and where val 1 to val n are the current values of the attributes att 1 to att n . The global state has the form {t}, where t is a term of sort Configuration that has the structure of a multiset of objects and messages, with multiset union denoted by a juxtaposition operator that is declared associative and commutative. A subclass inherits all the attributes and rules of its superclasses.
The dynamic behavior of concurrent object systems is axiomatized by specifying each of its transition patterns by a rewrite rule. For example, the rule A Real-Time Maude specification is executable, and the tool provides a variety of formal analysis methods. The rewrite command (trew t in time <= τ .) simulates one behavior of the system within time τ, starting with a given initial state t. The search command uses a breadth-first strategy to find n states reachable from the initial state t within time τ, which match a pattern and satisfy a condition. The Real-Time Maude's LTL model checker checks whether each behavior from an initial state, possibly up to a time bound, satisfies a linear temporal logic formula. State propositions are operators of sort Prop. A temporal logic formula is constructed by state propositions and temporal logic operators such as True,~(negation), /\, \/, -> (implication), [] ("always"), <> ("eventually"), U ("until"), and O ("next"). The command (mc t |=u ϕ in time <= τ .) checks whether the temporal logic formula ϕ holds in all behaviors up to duration τ from the initial state t.

The Airplane Turning Control System
This section presents a simple model of an avionics control system to turn an aircraft. In general, the direction of an aircraft is maneuvered by the ailerons and the rudder. As shown in Figure 2, an aileron is a flap attached to the end of the left or the right wing, and a rudder is a flap attached to the vertical tail (the aircraft figures in this section are borrowed from [7]). 116 3 Aerodynamics and Aircraft Control (c) Body axes are natural ones for the pilot and are the axes along which the inertia forces during manoeuvres (e.g. the normal acceleration during turns) are sensed. When an aircraft makes a turn, the aircraft rolls towards the desired direction of the turn, so that the lift force caused by the two wings acts as the centripetal force and the aircraft moves in a circular motion. The turning rate dψ can be given as a function of the aircraft's roll angle φ : where ψ is the direction of the aircraft, g is the gravity constant, and v is the velocity of the aircraft [7]. The ailerons are used to control the rolling angle φ of the aircraft by generating different amounts of lift force in the left and the right wings. Figure 3 describes such a banked turn using the ailerons. on the other wing is decreased and a rolling moment is thus generated. The rolling moment due to the rate of roll, p, acts in the opposite sense to the direction of rolling and is equal to L p p where L p is the rolling moment derivative due to rate of roll. Yawing moment derivative due to rate of roll N p . The rate of roll which increases the lift on the outer part of one wing and reduces it on the other also creates a differential drag effect. The increase in lift is accompanied by an increase in drag in the forward direction and the decrease in lift on the other wing by a corresponding reduction in drag. A yawing moment is thus produced by the rate of roll, p, which is equal to N p p where N p is the yawing moment derivative due to rate of roll.

Aircraft Dynamics 129
Yawing moment derivative due to rate of yaw N r . The rate of yaw, r, produces a tangential velocity component equal to l f r where l f is the distance between the aerodynamic centre of the fin and the yaw axis through the CG. The resulting change in the effective fin incidence angle, l f r/V T , produces a lift force which exerts a damping moment about the CG opposing the rate of yaw. The yawing moment due to the rate of yaw is equal to N r r where N r is the yawing moment derivative due to rate of yaw.
Rolling moment derivative due to rate of yaw L r . When the aircraft yaws, the angular velocity causes one wing to experience an increase in velocity relative to the airstream and the other wing a decrease. The lift on the leading wing is thus increased and the trailing wing decreased thereby producing a rolling moment. The rolling moment derivative due to rate of yaw is denoted by L r and the rolling moment due to rate of yaw is equal to L r r.
Lateral control derivatives due to ailerons and rudder. The ailerons and rudder are illustrated in Thus the acceleration towards the centre of the turn is g tan .
Referring to the inset vector diagram in Figure 3.33, the normal acceleration component is thus equal to g sec . Thus a 60 • banked turn produces a centripetal acceleration of 1.73g and a normal acceleration of 2g. At a forward speed of 100 m/s (200 knots approx.) the corresponding rate of turn would be 10.4 • /s. The lift required from the wings increases with the normal acceleration and the accompanying increase in drag requires additional engine thrust if the forward speed is to be maintained in the turn. The ability to execute a high g turn thus requires a high engine thrust/aircraft weight ratio.
To execute a coordinated turn with no sideslip requires the operation of all three sets of control surfaces, that is the ailerons and the tailplane (or elevator) and to a lesser extent the rudder. It is also necessary to operate the engine throttle(s) to control the engine thrust. The pilot first pushes the stick sideways to move the ailerons so that the aircraft rolls, the rate of roll being dependent on the stick movement. The rate of roll is arrested by centralising the stick when the desired bank angle for the rate of turn has been achieved. The pilot also pulls back gently on the stick to pitch the aircraft up to increase the wing incidence and hence the wing lift to stop loss  Side force derivative due to sideslip velocity Y v . The change in sideslip velocity, v, during a disturbance changes the incidence angle, β, of the aircraft's velocity vector, V T , (or relative wind) to the vertical surfaces of the aircraft comprising the fin and fuselage sides (see Figure 3.21). The change in incidence angle v/V T results in a sideways lifting force being generated by these surfaces. The net side force from the fuselage and fin combined is equal to Y v v where Y v is the sideforce derivative due to the sideslip velocity.
Yawing moment derivative due to sideslip velocity N v . The side force on the fin due to the incidence, β, resulting from the sideslip velocity, v, creates a yawing However, the rolling of the aircraft causes a difference in drag on the left and the right wings, which produces a yawing moment in the opposite direction to the roll, called adverse yaw. This adverse yaw makes the aircraft sideslip in a wrong direction with the amount of the yaw angle β , as described in Figure 4. This undesirable side effect is usually countered by using the aircraft's rudder, which generates the side lift force on the vertical tail that opposes the adverse yaw. To turn an aircraft safely and effectively, the roll angle φ of the aircraft should be increased for the desired direction while the yaw angle β stays at 0.
Such a roll and yaw can be modeled by simple mathematical equations under some simplifying assumptions, including: (i) the aircraft's wings are flat with respect to the horizontal axis of the aircraft, (ii) the altitude of the aircraft does not change, which can be separately controlled by using the aircraft's elevator (a flap attached to the horizontal tail of the aircraft), (iii) the aircraft maintains a constant speed by separately controlling the thrust power of the aircraft, and (iv) there are no external influences such as wind or turbulence. Then, the roll angle φ and the yaw angle β can be modeled by the following equations [2]: The lift force from the left, the right, or the vertical wing is given by the following linear equation: where, for Lift Right and Lift Left, Angle is the angle of the aileron, and for Lift Vertical, Angle is the angle of the rudder. The lift constant depends on the geometry of the corresponding wing, and the drag ratio is given by the size and the shape of the entire aircraft. We model the airplane turning control system as a multirate ensemble with 4 typed machines: the main controller, the left wing controller, the right wing controller, and the rudder controller. The environment for the airplane turning control system is given by the pilot console, which is modeled as another typed machine and is connected to the main controller on the outside of the control system. Each subcontroller moves the surface of the wing towards the goal angle specified by the main controller, which sends the desired angles to the sub-controllers to make a coordinated turn whose goal direction is specified from the pilot console. The main controller also models position sensors that measure the roll, the yaw, and the direction by using the aeronautics equations above. In this case study, we assume that the main controller has period 60 ms, the left and the right wing controllers have period 15 ms (rate 4), and the rudder controller has period 20 ms (rate 3). Our model is a two-level hierarchical multirate ensemble, since the airplane turning control system itself forms a single typed machine with period 60 ms (rate 10) and then is connected to the pilot console with period 600 ms, as illustrated in Figure 5.  Using the framework introduced in Section 4 for specifying and executing multirate synchronous ensembles in Real-Time Maude, we specify in Section 5 (and redefine in Section 6) the multirate ensemble E corresponding to the above airplane control system. In Section 6 we then exploit the bisimulation E MA (E, T, Γ) (see [4]) to verify properties about the asynchronous realization MA (E, T, Γ) by model checking them on the much simpler system E.

Multirate Synchronous Ensembles in Real-Time Maude
We have defined a framework for formally modeling and analyzing multirate ensembles in Real-Time Maude. Given a specification of deterministic single typed machines, their periods, input adaptors, a wiring diagram, and one top-level nondeterministic environment, our framework gives an executable Real-Time Maude model of the synchronous composition of the ensemble. It is natural to assume that controller components are deterministic; however, if we have a nondeterministic component, our framework could be modified so that local transitions are modeled by rewrite rules instead of equationally defined functions. If the system has "local" fast environments, they should be dealt with by the corresponding fast machines. 4 This section gives a brief overview of our framework and of how the user should specify the ensemble; the entire definition of our framework is given in our longer report [3].
Representing Multirate Ensembles in Real-Time Maude. The multirate ensemble can be naturally specified in an object-oriented style, where its machines and the ensemble can be modeled as objects. A typed machine is represented as an object instance of a subclass of the base class Component, which has the common attributes rate, period, and ports. The period denotes the period of the typed machine, and rate denotes its rate in a multirate ensemble. The ports attribute contains the input/output "ports" of a typed machine, represented as a multiset of Port objects, whose content attribute contains the data content as a list of values of the supersort Data: class Port | content : List{Data} . class InPort . class OutPort . subclass InPort OutPort < Port .
For each typed machine, the user must define an appropriate subclass of the class Component, the function delta defining its transition function, and the adaptor function for each input port: where the sort NeList{Data} denotes a non-empty list of data.
A multirate machine ensemble is modeled as an object instance of the class Ensemble. We support the definition of hierarchical ensembles by letting an ensemble be a Component, which also contains the wiring diagram (connections) and the machines in the ensemble. In this case, the ports attribute represents the environment ports of the ensemble: A wiring diagram is modeled as a set of connections. A connection from an output port P 1 of a component C 1 to an input port P 2 of a component C 2 is represented as a term C 1 .P 1 --> C 2 .P 2 . Similarly, a connection between an environment port P 1 and a machine port P 2 of a subcomponent C 2 is represented as a term P --> C 2 .P 2 (for an environment input) or a term C 2 .P 2 --> P (for an environment output).
Defining Synchronous Compositions of Multirate Ensembles. Given these definitions of an ensemble, our framework defines its synchronous composition as follows. The function delta of a multi-rate machine ensemble E defines the transitions in the synchronous composition of E. eq delta(< C : Ensemble | >) = transferResults(execute(transferInputs(< C : Ensemble | >))) .
In the above equation, the function transferInputs first transfers to each input port a value in the corresponding environment output port or the feedback output port. The execute function below applies the appropriate input adaptor to each sub-component, and then performs the function delta of each component as many times as its deceleration rate. Finally, the new outputs in sub-components are transferred to the environment ports by the function transferResults. eq execute(< C : Ensemble | machines : COMPS >) = < C : Ensemble | machines : executeSub(COMPS) > . eq executeSub(< C : Component | > COMPS) = k-delta(applyAdaptors(< C : Component | >)) executeSub(COMPS) . eq executeSub(none) = none .
The rates and periods should be consistent in an ensemble; that is, if some component has rate k and period p, then any component with rate k · t in the same ensemble should have period p/t.
Formalizing the Synchronous Steps. When each typed machine is deterministic and the system contains one (nondeterministic) top-level environment, the dynamics of the entire system given by a multirate machine ensemble is specified by the following tick rewrite rule that simulates each synchronous step of the composed system: These values are inserted into the appropriate component input port by the envOutput function, after clearing the outputs generated in the previous round by the clearOutputs function.
The delta function is finally applied to perform the transition of the component. Since an ensemble is an instance of the Component class and the delta function is also given for the Ensemble class, this tick rewrite rule can also be applied to a hierarchical multirate ensemble. After each synchronous step, the input ports of the component contain the environment input given by the possibleEnvOutput, and the output ports will have the resulting environment output generated by the delta function. The period does not have any effect on the structure of the transition system, but can be useful to verify timed properties, such as time-bounded LTL properties and metric CTL properties [8].

Modeling the Airplane Turning Control System
In this section we formally specify the airplane turning control system in Section 3 using the ensemble framework in Real-Time Maude described in Section 4. The entire specification is available in our report [3]. The following parameters are chosen to be representative of a small general aviation aircraft. The speed of the aircraft is assumed to be 50 m/s, and the gravity constants is g = 9.80555 m/s 2 . eq planeSize = 4.0 . eq weight = 1000.0 . eq wingSize = 2.0 . eq virtLiftConst = 0.6 . eq horzLiftConst = 0.4 . eq dragRatio = 0.05 .
Subcontroller. The subcontrollers for the ailerons and the rudder are modeled as object instances of the following class SubController: class SubController | curr-angle : Float, goal-angle : Float, diff-angle : Float . subclass SubController < Component .
A subcontroller increases/decreases the curr-angle toward the goal-angle in each round, but the difference in a single (fast) round should be less than or equal to the maximal angle diff-angle. The transition function delta of a subcontroller is then defined by the following equation: The velocity attribute denotes the speed of the aircraft. The curr-yaw, curr-roll, and curr-dir attributes model the position sensors of the aircraft by indicating the current yaw angle β , roll angle φ , and direction Ψ, respectively. The goal-dir attribute denotes the goal direction given by the pilot.
For each round of the main controller, the attributes curr-yaw, curr-roll, and curr-dir are updated 5 using the angles of the wings in the input ports that are transferred from the subcontrollers. The goal-dir is also updated if a new goal direction arrives to the input ports. Based on the new current position status and the goal direction, the new angles of the wings are evaluated and sent back to the subcontrollers. The transition function delta of the main controller is then defined as follows: The first four lines in the condition compute new values for curr-yaw, curr-roll, curr-dir, and goal-dir, based on values in the input ports. A non-⊥ value in the port input is added to goal-dir. The variables RA' and TA' denote new angles of the ailerons and the rudder, computed by the control functions explained below. Such new angles are queued in the corresponding output ports, and will be transferred to the related subcontrollers at the next synchronous step since they are feedback outputs. The last line in the condition gives the output for the current step, the new position information of the aircraft, which will be transferred to its container ensemble at the end of the current synchronous step.
The new angles of the ailerons and the rudder are computed by the control functions. The function horizWingAngle computes the new angle for the aileron in the right wing, based on the current roll angle and the goal roll angle. The angle of the aileron in the left wing is always exactly opposite to the one of the right wing. The function goalRollAngle computes the desired roll angle φ to make a turn, based on the current roll angle and the difference between the goal direction and the current direction. Finally, in order to achieve a coordinated turn where the yaw angle is always 0, the function tailWingAngle computes the new rudder angle based on the current yaw angle. We define all three control functions by simple linear equations as follows, where CR is a current roll angle and CY is a current yaw angle: eq goalRollAngle(CR,CD,GD) = sign(angle(GD -CD)) * min(abs(angle(GD -CD)) * 0.3, 20.0) . eq horizWingAngle(CR,GR) = sign(angle(GR -CR)) * min(abs(angle(GR -CR)) * 0.3, 45.0) . eq tailWingAngle(CY) = sign(angle(-CY)) * min(abs(angle(-CY)) * 0.8, 30.0) .
That is, the goal roll angle is proportional to the difference GD − CD between the goal and current directions with the maximum 20 • . The horizontal wing (aileron) angles are also proportional to the difference GR − CR between the goal and current roll angles with the maximum 45 • . Similarly, the rudder angle is proportional to the difference − CY between the goal and current yaw angles with the maximum 30 • , where the goal yaw angle is always 0 • .
Pilot Console. The pilot console, the environment for the aircraft turning control system, is modeled as an object instance of the following class PilotConsole: class PilotConsole | scenario : List{Data} . subclass PilotConsole < Component .
The attribute scenario contains a list of goal angles that are transmitted to the main controller. The transition function delta of the pilot console keeps sending goal angles in the scenario to its output port until no more data remains in the scenario. In addition, the pilot console has an extra input port to receive an outer environment input to generate nondeterministic goal directions. A non-⊥ value in the input port is added to the output given by the scenario. If the scenario is empty, i.e., nil, the outer environment input is ignored, and the pilot console will keep sending ⊥ to its output port.
Airplane System. The entire architecture of the airplane turning control system in Figure 5, including the environment (i.e., the pilot console), is then represented as an ensemble object with subcomponents as follows (some parts of the specification are replaced by '...'): The top-level ensemble airplane includes the pilot console pilot and the ensemble csystem for the airplane turning control system. The airplane has one input port for the pilot console to generate nondeterministic goals, and one output port to display the result.
In the ensemble csystem, the input adaptors for the subcontrollers generate a vector with extra ⊥'s and the adaptor for the main controller selects the last value of the input vector. The function bots(n) generates n ⊥-constants. Similarly, in the top ensemble airplane, the input adaptor for the ensemble csystem generates a vector with extra ⊥'s, and the adaptor for the pilot console selects the last value of the input vector. eq adaptor(csystem, input, D) = D bots(9) eq adaptor(pilot, input, LI D) = D .

Formal Analysis of the Airplane Turning Control System
This section explains how we have formally analyzed the above Real-Time Maude model of the multirate synchronous design of the airplane turning control system, and how the turning control system has been improved as a result of our analysis. Multirate PALS ensures that the verified properties also hold in a distributed real-time realization of the design. There are two important requirements that the airplane turning control system should satisfy: • Liveness: the airplane should reach the goal direction within a reasonable time with a stable status in which both the roll angle and the yaw angle are close to 0.
• Safety: during a turn, the yaw angle should always be close to 0.
We first analyze deterministic behaviors when the airplane turns +60 • to the right. 6 In this case, there are no outer environment inputs to the pilot console, so that the pilot console sends the goal angles in the scenario to the main controller in turn. We consider the following three scenarios: 1. The pilot gradually increases the goal direction in 6 seconds, +10 • for each second.
2. The pilot sets the goal direction to +60 • at the first step.
3. The goal direction is at first −30 • , and then it is suddenly set to +60 • in one second.  For example, the scenario 3 is represented as the term "d(-30.0) d(90.0)" for a list of directions. As we can see in the graph, the airplane reaches the goal direction 60 • in a fairly short time, and the roll angle also goes to a stable status. However, the yaw angle seems to be quite unstable.
There are basically two reasons why the yaw angle is not sufficiently close to 0 during a turn. First, since all control functions are linear, the new angles for the ailerons and the rudder are not small enough when the yaw angle is near 0. Second, the roll angle is sometimes changing too fast, so that the rudder cannot effectively counter the adverse yaw. Therefore, we modify the control functions as follows: When the difference between the goal and the current angles (i.e., FR or FY) is less than or equal to 1, the functions horizWingAngle and tailWingAngle are now not proportional to the difference, but proportional to the square of it. Furthermore, the goal roll angle can be changed at most 1.5 • at a time, so that there is no more abrupt rolling. In order to check if the new control functions are safe, we define some auxiliary functions. The function PortId ?= Component returns the content of the corresponding port in the Component: eq P ?= < C : Component | ports : < P : Port | content : DL > PORTS > = DL . and the function safeYawAll(OutputDataList) checks whether every output data in the given list has a safe yaw angle, namely, an angle less than 1.0 • . eq safeYawAll(DO LI) = abs(yaw(DO)) < 1.0 and safeYawAll(LI) . eq safeYawAll(nil) = true .

No solution
Although each state of the transition system captures only the slow steps for the top ensemble (i.e., every 600ms), safeYawAll also checks all fast steps for the main controller (every 60ms), since it accesses the history of the main controller's status in the output port of the top ensemble, which the main controller sends to the top ensemble for each fast step of it. Furthermore, we can use Real-Time Maude's LTL model checking to verify both liveness and safety at the same time. The desired property is that the airplane reaches the desired direction with a stable status while keeping the yaw angle close to 0, which can formalized as the LTL formula (¬stable → (safeYaw U (reach ∧ stable))) where the atomic propositions safeYaw, stable, and reach are defined as follows: The following model checking command then shows that our redesigned system, with the new control functions, satisfies the above LTL property within 18 seconds, where one of the above five angles is nondeterministically chosen and added to the angle 0 • in the scenario for each step of the pilot console: The number of states explored in this model checking analysis is 246, 785, 7 which is a huge state space reduction compared to the distributed asynchronous model since: (i) asynchronous behaviors are eliminated thanks to PALS, and (ii) any intermediate fast steps for the sub-components are merged into a single-step of the system's top-level ensemble.

Conclusions
The present work can be seen from different perspectives. First, from the perspective of research on the PALS methodology, its main contribution is to demonstrate that Multirate PALS, when used in combination with a tool like Real-Time Maude, can be effectively applied to the formal verification of nontrivial DCPS designs, and even to the process of refining a DCPS design before it is verified. Second, from the perspective of the formal specification and verification of distributed hybrid systems, it also shows that Real-Time Maude is an effective tool for specifying and verifying such systems.
Much work remains ahead. On the one hand, more case studies like this one should be developed. On the other hand, our work in [5], which applies PALS to a synchronous fragment of the AADL CPS modeling language in the single rate case, should be extended to the Multirate PALS case. Finally, the hybrid system applications of Real-Time Maude should be further developed independently of PALS. Several such applications have been developed in the past; but many more are possible, and a richer experience will be gained.