Multi-University Research Initiative on High-Confidence Design for Distributed Embedded Systems Frameworks and Tools for High-Confidence Design of Adaptive, Distributed Embedded Control Systems Year 3 Progress Report Vanderbilt University Institute for Software Integrated Systems 2015 Terrace Place, Nashville, TN 37203 (615) 322-3455 (office) (615) 343-7440 (fax) [email protected] TEAM MEMBERS: Vanderbilt: J. Sztipanovits (PI) and G. Karsai UC Berkeley: C. Tomlin (Lead and co-PI), Edward Lee and S. Sastry CMU: Bruce Krogh (Lead and co-PI) and Edmund Clarke Stanford: Stephen Boyd FA9550-06-0312 Report Documentation Page Form Approved OMB No. 0704-0188 Public reporting burden for the collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources, gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection of information, including suggestions for reducing this burden, to Washington Headquarters Services, Directorate for Information Operations and Reports, 1215 Jefferson Davis Highway, Suite 1204, Arlington VA 22202-4302. Respondents should be aware that notwithstanding any other provision of law, no person shall be subject to a penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number. 1. REPORT DATE 3. DATES COVERED 2009 2. REPORT TYPE 00-00-2009 to 00-00-2009 4. TITLE AND SUBTITLE 5a. CONTRACT NUMBER Frameworks and Tools for High-Confidence Design of Adaptive, 5b. GRANT NUMBER Distributed Embedded Control Systems 5c. PROGRAM ELEMENT NUMBER 6. AUTHOR(S) 5d. PROJECT NUMBER 5e. TASK NUMBER 5f. WORK UNIT NUMBER 7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES) 8. PERFORMING ORGANIZATION Vanderbilt University,Institute for Software Integrated Systems,2015 REPORT NUMBER Terrace Place,Nashville,TN,37203 9. SPONSORING/MONITORING AGENCY NAME(S) AND ADDRESS(ES) 10. SPONSOR/MONITOR’S ACRONYM(S) 11. SPONSOR/MONITOR’S REPORT NUMBER(S) 12. DISTRIBUTION/AVAILABILITY STATEMENT Approved for public release; distribution unlimited 13. SUPPLEMENTARY NOTES 14. ABSTRACT 15. SUBJECT TERMS 16. SECURITY CLASSIFICATION OF: 17. LIMITATION OF 18. NUMBER 19a. NAME OF ABSTRACT OF PAGES RESPONSIBLE PERSON a. REPORT b. ABSTRACT c. THIS PAGE Same as 21 unclassified unclassified unclassified Report (SAR) Standard Form 298 (Rev. 8-98) Prescribed by ANSI Std Z39-18 1. Objectives This project aims to develop a comprehensive approach to the model-based design of high- confidence distributed embedded systems. We will take advantage and fully leverage a shared theoretical foundation and technology infrastructure in four focus areas: hybrid and embedded systems theory, model-based software design, composable tool architectures and experimental testbeds. The objectives of our research in the focus areas are the following: 1. Develop theory of deep composition of hybrid systems with attributes of computational and communication platforms. We will address compositionality, concurrency, heterogeneity and resource, robustness, approximate verification and adaptive control architectures for uncer- tainty handling. 2. Develop foundations of model-based software design for high-confidence, networked em- bedded systems applications. We will investigate new semantic foundations for modeling languages and model transformations, precisely architected software and systems platforms that guarantee system properties via construction, and new methods for static source code ve- rification and testing, as well as for dynamic runtime verification and testing. 3. Develop composable tool architecture that supports high-level reusability of modeling, mod- el-analysis, verification and testing tools in domain-specific tool chains. We create new foundation for tool integration that goes beyond data modeling and data transfer. 4. Demonstrate the overall effort by creating an end-to-end design tool chain prototype for the model-based generation and verification of embedded controller code for experimental plat- forms. 2. Status of the Effort We have reached the following major milestones toward the compositional design of high confidence embedded control systems on computational and communication platforms. 1. We have achieved new results in hybrid control system design using reachable set analysis: a methodology for computing reachable sets using quantized inputs over discrete time steps has been developed and implemented for an aircraft collision avoidance example. We have used reachable set analysis in complex control law de- sign, and have demonstrated its use (in simulation) on aerobatic maneuver design for the STARMAC quadrotor helicopter testbed. In related work, we have developed a new optimization scheme for scheduling hybrid systems, and have demonstrated the results on an autonomous car simulation testbed. We are focusing efforts this summer for both projects in demonstration of the algorithms on the actual testbeds. 2. We have extended our approach for integrated software model checking in the loop to the case of nonlinear dynamic plant models using the concept of bisimulation func- tions for nonlinear systems. 3. We developed a new widening operator for verification of numerical programs that is much less conservative than standard widening operators used to accelerate the termi- nation of fixed point computations in abstract interpretation. We initiated work on ar- 2 chitecture-level tools for modeling and verifying properties of embedded system de- sign specifications early in the design process. 4. We have continued developing the passivity based approach for networked controller design and demonstrated feasibility experimentally. 5. We have completed the working prototype of an end-to-end tool chain for the model- based design of networked control systems. The toolchain integrates a verification step to verify code ‘as running on the physical platform’. The underlying implementation platform is the Time-Triggered Architecture (TTA), realized on two processor types and communication buses. We have built demonstrations for auto-generating code from verified models. 6. Translating models into efficient executable embedded code that reliably implements the model semantics continues to be a challenging problem. We have re-architected the Ptolemy II code generation infrastructure to provide an adaptable and extensible platform that supports experimentation with code generation for a variety of models of computation and target platforms. We are using and extending this framework to build code generators based on synchronous dataflow, finite state machine, synchron- ous/reactive, Giotto, and Ptides models of computation, and have shown that we can target bare-iron microcontrollers, lightweight microkernels, and real-time operating systems. 3. Accomplishments and New Findings We continued our work on developing tools, methods and other components of the project along the four objectives. 3.1 Hybrid and Embedded Systems Theory 3.1.1 Embedded Systems Modeling and Deep Compositionality (Krogh, Tomlin, Sastry) While our progress in previous years has focused on the computation and use of reachable sets for simple protocol verification and analysis, over this past year we have begun to develop a method for hybrid system trajectory planning, using the high level mode description. Related re- search efforts in the past have developed symbolic languages for robot motion planning, for de- scribing complex system behavior, or estimating behavior from observation, this is the first time that the broad concept of reachable sets has been used to provide a priori verified behavior, at the planning level. We have demonstrated the technique in simulation on a challenging problem (aerobatic maneuvers for our STARMAC quadrotor platform), and we are currently working on the actual flight implementation. 3.1.2 Hierarchies of Robust Hybrid and Embedded Systems (Tomlin, Krogh, Sastry) Reachability analysis. We have extended our technology for reachable set design to include quantized input signals, and discrete time implementation. This makes the technique much more useful in practice. We have implemented this extension on simulation examples of collision avoidance for two civilian aircraft, and an automated re-fueling example involving a UAV and a large tanker. We have also developed methods for path planning around reachable sets: using a 3 combination of forward reachable set computation, and convex underapproximation of the region around reachable sets, we have shown how the trajectory planning method can be posed as a convex optimization program. Optimization of hybrid systems. We have developed an optimal control algorithm for switched hybrid systems, which given a cost function and a set of inequality constraints computes the op- timal sequence of discrete states, the optimal times for switches between discrete states, and the optimal continuous input for each state. Our method is iterative, involving updates on the optimal mode switch time by perturbing an initial switch schedule, therefore the results from our method are only locally optimal. We have implemented this scheme in simulation on an automated car testbed, using our method as a trajectory planner, and we expect to use this algorithm in a real car in the future. 3.1.3 Constructive Architectures for Digital Controllers of Continuous Time Systems (Kottens- tette) Using passivity and scattering theory we have shown how to interconnect either a linear or non-linear passive continuous time system to a passive digital controller in which continuous time stability (L 2-stability) can be guaranteed. The key to creating such a system is to transform m the continuous time input-output signals of the plant to wave-variables. The continuous-time wave variables are then interfaced to a passive sampler (PS) which converts a continuous-time- wave-variable to a discrete-time-wave-variable in a causal manner at an arbitrary sampling rate T , analogously a passive hold (PH) converts a discrete-time-wave-variable to a continuous-time- s wave-variable in a passive manner at an update rate T. These discrete-time wave-variables can s then be transmitted over a digital network and in-spite fixed-time delays and data-dropouts of the wave-variables L 2-stability can be preserved. In fact, time delays, such as those incurred over m TCP/IP communication networks, can be tolerated without any modification to the original sys- tem. Other communications protocols such as UDP can also be used as long as duplicate wave- variable transmissions are dropped. We have successfully applied this architecture to both linear and non-linear systems including robotic-arm-manipulators. In order to show L 2-stability, an m important analysis tool, which we refer to as the inner-product-equivalent-sampler and zero- order-hold (IPESH), is used to relate non-wave-continuous-time variables to non-wave-discrete- time variables. In fact, the IPESH-transform now makes it possible to synthesize discrete-time linear-time-invariant controllers which closely match their continuous-time counterpart in both magnitude and phase response up to the Nyquist frequency (π/T ) without any need for ‘pre- s warping’. The IPESH-transform, makes it extremely easy to generate a digital controller which can cancel out non-ideal lag effects such as those encountered by the rotor-angular-velocity to rotor-thrust characteristics associated with quad-rotor aircraft. This passivity based frame-work has been successfully applied to the control of multiple-plants and controllers. In particular we have shown how a power junction can be used to interconnect multiple-plants and controllers while preserving system stability. The averaging-power junction has been shown to allow mul- tiple continuous-time plants with the same steady-state gain (yet different dynamic transients) to be commanded by a single PID-digital-controller to track a given trajectory. Furthermore, through the use of a resilient power junction we have shown how a digital control network can be constructed in which redundant passive-digital controllers can be lost and even corrupted while preserving over-all system stability. 4 Using conic-systems theory, a more generalized form of passivity theory, we have shown how stabilizing controllers for systems consisting of cascades of passive-sub-systems such as the quad-rotor aircraft can be constructed. In fact, the overall control-architecture essentially con- sists of nested diagonal proportional feedback control loops and a single saturation block to ac- count for actuator saturation limits. In spite of the broad applicability to both linear and non- linear systems, the advantages of the control-architecture include being easy to construct and un- derstand, requires a minimal-amount of mathematical operations, and possess significant robust- ness to system uncertainty. For example, in practice, we have found our architecture to be quite insensitive to modest sampling rate and delay even when applied to the control of non-linear sys- tems such as the quad-rotor aircraft 3.1.4 Verification and Validation of Conservative Approximations (Clarke, Krogh) Bounded-time verification technique that combines software model checking and simulation. We extended our method for integrating source-code model checking with dynamic system anal- ysis to verify properties of controllers for nonlinear dynamic systems. Source-code model checking verifies the correctness of control systems including features that are introduced by the software implementation, such as concurrency and task interleaving. Sets of reachable conti- nuous state variables are computed using numerical simulation and bisimulation functions. The technique as originally proposed handles stable dynamic systems with affine state equations for which quadratic bisimulation functions can be computed easily. The extension in this past year handles nonlinear systems with polynomial state equations for which bisimulation functions can be computed in some cases using sum-of-squares (SoS) techniques. The algorithm includes the convex optimizations required to perform control system verification using a source-code model checker, and the method is illustrated for an example of a supervisory control system. Systematic search for counterexamples using model checking and numerical simulation. We extended the trajectory sensitivity work to a parameter synthesis problem for nonlinear hybrid systems. Considering a set of uncertain parameters and a safety property, we give an algorithm that returns a partition of the set of parameters into subsets classified as safe, unsafe, or uncer- tain, depending on whether respectively all, none, or some of their behaviors satisfy the safety property. We make use of sensitivity analysis to compute approximations of reachable sets and an error control mechanism to determine the size of the partition elements in order to obtain the desired precision. We apply the technique to Simulink models by combining generated code with a numerical solver that can compute sensitivities to parameter variations. We present experimen- tal results on a non-trivial Simulink model of a quadrotor helicopter. 3.1.5 Statistical Probabilistic Model Checking (Clarke, Platzer) Stochastic systems arise naturally, for example, because of uncertainties present in a system’s environment (e.g., the reliability of communication links in a wireless sensor network, the rate of message arrivals on an aircraft’s communication bus, or the number of contenting peers in a Blu- etooth device discovery phase). Uncertainty is usually modeled via a probability distribution, thereby resulting in stochastic systems, i.e., systems which exhibit probabilistic behavior. These are clearly very important systems with many practical applications, which motivated our inves- tigation on how Model Checking can be applied to stochastic systems. The problem of Model Checking stochastic systems is quite different from the Model Checking of standard systems. Because of the probabilistic behavior, one has to introduce a notion of probability in the concept 5 “the system satisfies a specification”. Suppose we are given a temporal logic formula f and a closed (i.e., with no free parameters or inputs) stochastic system M. Then we can assign a unique probability p to the event “system M satisfies property f”. The following question is now well- posed: is p greater (or smaller) than t (where t is a user-defined threshold probability, which in general depends on the property being verified)? The Probabilistic Model Checking problem thus amounts to finding out whether a system satisfies a specification with at least (or at most) a fixed probability. For example: “does the system fulfill a request within 1ms with probability at least 0.99?” Numerical methods solve the Probabilistic Model Checking problem by first computing the (unknown) probability p and then comparing it with the threshold t. However, these methods do not scale up to realistic systems. Our solution to the Probabilistic Model Checking problem is in- stead based on randomized sampling of the system’s traces and statistical hypothesis testing. Therefore, the statistical conclusion is not guaranteed to be correct, but the probability of giving a wrong answer is bounded. The benefit of our approach is that a conclusion is often reached significantly faster than with numerical techniques, thus making the approach more scalable to the challenging size and complexity of our target systems. We have successfully applied our approach to a model of a Delta-Sigma modulator for which previous formal verification attempts were too conservative and required excessive computation time. We have also started investigating the use of Statistical Probabilistic Model Checking for the verification of Stateflow-Simulink models with a hybrid dynamics. In particular, we have de- veloped a new algorithm for solving the Probabilistic Model Checking problem. The algorithm uses a statistical sequential approach based on Bayes’s theorem. The sequential character of our approach means that the number of sampled traces is not fixed a priori, but it is instead deter- mined at “run-time”. The use of Bayes’s theorem enables our algorithm to take advantage of previous knowledge about the model, where available. We have showed that, on several repre- sentative examples, our algorithm generally leads to faster verification than state-of-the-art ap- proaches, based on either statistical or numerical techniques. These very encouraging results show that Model Checking techniques are likely to scale up to real-world hybrid systems. 3.1.6 Verification of Hybrid Systems via Differential Invariants (Clarke, Platzer) In air traffic control, collision avoidance maneuvers are used to resolve conflicting flight paths that arise during free flight. Aircraft collision avoidance maneuvers are important and complex applications. Several maneuvers have been proposed already that assume instant turns in mid flight. Real aircraft, however, can only follow sufficiently smooth flyable curves. Hence, mathematical maneuvers that require instant turns give physically impossible conflict resolution advice. Yet curved flight exhibits nontrivial continuous behavior. In combination with the con- trol choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we have analyzed collision freedom of roundabout maneuvers in air traffic control. In this domain, appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We have shown that for- mal verification of hybrid systems can scale up to curved flight maneuvers required in aircraft control applications. We have introduced a fully flyable variant of the roundabout collision avoidance maneuver and verified safety properties by compositional verification. In contrast to other approaches, we verify the hybrid system dynamics without solving the differential equations and without numer- 6 ical errors. We use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixed-point algorithm works with a compositional verification logic for hybrid systems. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification proce- dure, and achieve better automation. These results indicate that hybrid systems are a promising direction of further research for the aviation domain, including unmanned aerial vehicles 3.2 Model-Based Software Design and Verification 3.2.1 Model-Integrated Computing (Sztipanovits, Karsai, Kottenstette) Cross-layer abstractions. Model - based software design progresses along abstraction layers (design platforms) capturing essential design concerns. Effectiveness of the model-based design largely depends on how much the design concerns (captured in the abstraction layers) are ortho- gonal, i.e., how much the design decisions in the different layers are independent. Heterogeneity of embedded systems causes major difficulties in this regard. The controller dynamics is typical- ly designed without considering implementation side effects (e.g. numeric accuracy of computa- tional components, timing accuracy caused by shared resource and schedulers, time varying de- lays caused by network effects, etc.). Compositionality in one layer depends on a web of assump- tions to be satisfied by other layers. We have continued investigating theories and techniques for applying cross-layer abstraction to make the controller designs robust against implementation side effects. We pursue this by in- serting implementation related abstractions in the controller design, and physical abstractions in software design. The ultimate goal is decreasing the entanglement across the design layers. We have developed model transformation tools that generate TrueTime abstractions from sys- tem level models and investigate now the application of orthogonal structures in implementing dynamics. 3.2.2 Autocoding Embedded software for Safety Critical Systems (Lee) Professor Lee's group at Berkeley has furthered the development of semantic-preserving code generation in two areas: (1) code generation of Giotto models using the Precision Timed (PRET) Architecture and (2) Compositional Code Generation. As part of her Master's Thesis, Shanna-Shaye Forbes developed code generation from the Giotto model of computation in Ptolemy II to the Precision Timed (PRET) architecture. (cid:131) Giotto is a programming model for embedded control systems that is applicable to hard real-time specifications that are periodic and features multi-modal behavior. Examples of such systems include fly-by-wire or brake-by-wire systems where sensor readings must be periodic and there are multiple modes of operation. (cid:131) PRET is a computer architecture that emphasizes predictable timing. (cid:131) Ptolemy II is an open source modeling and simulation framework that supports model- based design, and facilitates actor oriented and objected oriented programming. It serves as a laboratory for the modeling and simulation necessary in the design of a real-time embedded system. Ptolemy II has an implementation of the Giotto pro- gramming model that allows the simulation of Giotto models in Ptolemy II. Ptolemy 7 II also has an extensible C code generation framework can be retargeted for different targets. In our code generation approach, we employ the correct-by-construction premise and make use of PRET's deadline capabilities to generate C code which fulfills the timing constraints of the model. We demonstrated our facility by running the generated code on the cycle-accurate PRET simulator which lets us verify that our designs meet the hard real-time deadlines. In addition to generating PRET code, we retargeted our Giotto code generation to OpenR- TOS, a real-time operating system for embedded platforms. To illustrate these techniques we ex- tend the code generation framework within Ptolemy II to generate C code for the Giotto pro- gramming model. We have implemented a C code generation adapter in Ptolemy II for the Giotto model of computation targeted to systems capable of running the OpenRTOS operating system. We presented an elevator controller as an example that uses the code generation framework. Bert Rodiers, Jackie Man-kit Leung and others have been developing Compositional Code Generation, which we define as the act of automatically generating code on a per composite actor basis. By generating code in this manner, we hope to be able to compose generated code with interpreted code in simulation, which will result in performance improvements for high perfor- mance models. Compositional Code Generation will also allow us to reuse auto generated code without regenerating it each time. Similar to the spirit of co-simulation, where subsystems are executed modularly, compositional code generation combined with semantic preservation allow us to retarget submodels to different contexts. This work is in progress, we are studying the modularity problem by advancing interface theories to describe our simulation and code genera- tion components. We are also refactoring our earlier code generation system and taking advan- tage of lessons learned, such as removing model of computation specific details from the code generation kernel. 3.2.3 Automated Source Code Verification and Testing (Clarke, Platzer, Krogh) Verification of numerical code. Verification of numerical code is an important problem in embedded systems since computational artifacts such as overflow, underflow, error accumula- tion, divide by zero, etc., which are not present in the idealized models used for algorithm de- sign, can lead to unexpected and possibly catastrophic consequences in many applications. We developed a static analysis technique for polyhedral domains to compute bounds on the variables in numerical code with linear arithmetic, and introduce a new widening operator that can be more precise than standard widening for iterative computations. We also developed heuristics for reducing the complexity of the analysis. 3.3 Composable Tool Architectures 3.3.1 Advanced Open Tool Integration Framework (Karsai, Sztipanovits) Formal specification of behavioral semantics. We have continued our efforts on the formal specification of behavioral semantics for domain specific modeling languages. In the last year we have started examining Sifakis’ Behavior-Interaction-Priority (BIP) model as an abstraction layer in the design flow. 3.3.2 Prototype Tool Chain (Volgyesi, Karsai, Sztipanovits) 8 Prototype toolchain. We continued our work on the prototype tool chain, based on the model- ing language ESMoL. The architecture of the tool chain is show in Figure 1, while Figure 2 shows the specific tools and logical flow across the tools. The tool chain is capable to work with high level (controller) models imported from the MATLAB/Simulink environment (MDL2MGA tool), partition and assign components to nodes and tasks (ESMoL domain specif- ic modeling language and the GME modeling environment) and generate code and runtime con- figuration for different distributed platforms (TTP/C, Linux, FreeRTOS). The code is generated in two steps; first the abstract syntax tree of the code is built (SL/SF CodeGen tools, SFC do- main specific modeling language), then the actual C/C++ (optionally: Java) code is printed from the abstract model (SFCPrint tool). The most important benefits are the relatively low cost of adding support for additional programming languages and high level access to the executable code for external tools (e.g. source code verification) The experimental platform includes a Linux-based TTA realization (the FRODO TTA virtual machine, running on a low-end Linux board, called the Gumstix platform) and a RTOS-based TTA realization (the same virtual machine, running on a low-end microcontroller board, called the Robostix platform). The same hardware platforms are used in the Stanford STARMAC ve- hicle. During the past years we have developed the platform-specific code generators that pro- duce integration code for these platforms (the functional code generators were implemented in previous years). We have developed the I/O drivers for the low-end controller that work with the time-triggered run-time scheduler. We have extended the design-time, offline scheduler to sche- dule the periodic message transfers on the shared bus, and to account for I/O overhead in the scheduling. Figure 1: Architecture of the tool chain 9