Translating Discrete Time SIMULINK To SIGNAL
Translating Discrete Time SIMULINK to SIGNALSafa MessaoudThesis submitted to the Faculty of theVirginia Polytechnic Institute and State Universityin partial fulfillment of the requirements for the degree ofMaster of ScienceinComputer EngineeringSandeep K. Shukla, ChairMichael S. HsiaoJoAnn M. PaulMay 28, 2014Arlington, VirginiaKeywords: SIMULINK, SIGNAL, Embedded Software, Code GenerationCopyright 2014, Safa Messaoud
Translating Discrete Time SIMULINK to SIGNALSafa Messaoud(ABSTRACT)As Cyber Physical Systems (CPS) are getting more complex and safety critical, Model BasedDesign (MBD), which consists of building formal models of a system in order to be used inverification and correct-by-construction code generation, is becoming a promising methodology for the development of the embedded software of such systems. This design paradigmsignificantly reduces the development cost and time while guaranteeing better robustness,capability and correctness with respect to the original specifications, when compared withthe traditional ad-hoc design methods. SIMULINK has been the most popular tool for embedded control design in research as well as in industry, for the last decades. As SIMULINKdoes not have formal semantics, the application of the model based design methodology andtools to its models is very limited. In this thesis, we present a semantic translator thattransform discrete time SIMULINK models into SIGNAL programs. The choice of SIGNALis motivated by its polychronous formalism that enhances synchronous programming withasynchronous concurrency, as well as, by the ability of its compiler of generating deterministic multi thread code. Our translation involves three major steps: clock inference, typeinference and hierarchical top-down translation. We validate the semantic preservation ofour prototype tool by testing it on different SIMULINK models.
ContentsContentsiiiList of FiguresviList of Tablesviii1 Introduction12 Background42.1Model Based Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .42.2SIMULINK . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .52.3Synchronous Programming Languages. . . . . . . . . . . . . . . . . . . . .62.4The Multi-rate Synchronous Language SIGNAL . . . . . . . . . . . . . . . .62.4.1Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .72.4.2The SIGNAL Formalism . . . . . . . . . . . . . . . . . . . . . . . . .82.4.3Advanced SIGNAL Constructs. . . . . . . . . . . . . . . . . . . . .102.4.4SIGNAL Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . .102.4.5Endochrony and Weak Endochrony . . . . . . . . . . . . . . . . . . .112.4.6Uses of SIGNAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13Comparison between SIMULINK and SIGNAL . . . . . . . . . . . . . . . . .132.53 Related Work3.114Translating SIMULINK to a Formal Language . . . . . . . . . . . . . . . . .iii14
3.1.1SIMULINK to LUSTRE . . . . . . . . . . . . . . . . . . . . . . . . .143.1.2SIMULINK to Synchronous BIP . . . . . . . . . . . . . . . . . . . . .153.2Translating SIMULINK to a Hybrid Automata . . . . . . . . . . . . . . . . .153.3Translating SIMULINK to a System of Equations . . . . . . . . . . . . . . .163.4Contribution of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . .184 Translating discrete time SIMULINK to SIGNAL204.1Translation Goals and Assumptions . . . . . . . . . . . . . . . . . . . . . . .204.2Translation Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .224.3Type Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .234.3.1Types in SIMULINK . . . . . . . . . . . . . . . . . . . . . . . . . . .234.3.2Types in SIGNAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . .234.3.3Type Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .244.4Type Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .284.5Clock Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .294.5.1Time in SIMULINK . . . . . . . . . . . . . . . . . . . . . . . . . . .294.5.2Time in SIGNAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . .314.5.3Clock Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .314.6Clock Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .344.7Basic SIMULINK Blocks translation . . . . . . . . . . . . . . . . . . . . . .364.8SubSystems translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .414.8.1Plain SubSystems Translation . . . . . . . . . . . . . . . . . . . . . .414.8.2Triggered SubSystems Translation . . . . . . . . . . . . . . . . . . . .424.8.3Enabled SubSystems Translation . . . . . . . . . . . . . . . . . . . .435 Case Studies455.1Closed Loop Controller . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .455.2Discretized DC-Motor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .475.3Discretized DC-Motor Closed Loop Controller . . . . . . . . . . . . . . . . .48iv
6 Conclusion526.1Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .526.2Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .536.3Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .536.4Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .54Bibliography56A Case Study 158B Case Study 261C Case Study 367v
List of Figures2.1The V Design Process. http://www.engineering.com/DesignSoftware. Usedunder fair use, 2014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .54.1Supported SIMULINK Blocks . . . . . . . . . . . . . . . . . . . . . . . . . .214.2Translation Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .224.3The Type Lattice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .244.4The Type Matrix Generation Example . . . . . . . . . . . . . . . . . . . . .254.5Type Inference (Example 1) . . . . . . . . . . . . . . . . . . . . . . . . . . .264.6Type Inference (Example 2) . . . . . . . . . . . . . . . . . . . . . . . . . . .284.7Type Inference (Example 3) . . . . . . . . . . . . . . . . . . . . . . . . . . .284.8Timing Mechanism in SIMULINK (Sample Time) . . . . . . . . . . . . . . .304.9Timing Mechanism in SIMULINK (Triggered Sub-System) . . . . . . . . . .304.10 Timing Mechanism in SIMULINK (Enabled Sub-System) . . . . . . . . . . .314.11 Example 1: Clock Inference Timing Error . . . . . . . . . . . . . . . . . . .324.12 Example 2: Clock Inference Timing Error . . . . . . . . . . . . . . . . . . .324.13 Example 3: Clock Inference . . . . . . . . . . . . . . . . . . . . . . . . . . .344.14 Clock Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .344.15 Triggered SubSystems Translation . . . . . . . . . . . . . . . . . . . . . . . .425.1Case Study 1: Closed Loop Controller. . . . . . . . . . . . . . . . . . . . .465.2Case Study 2: Discretized DC-Motor . . . . . . . . . . . . . . . . . . . . . .495.3Case Study 3: Discretized DC-Motor Closed Loop Controller . . . . . . . . .51vi
6.1Example of an Enabled SubSystem . . . . . . . . . . . . . . . . . . . . . . .546.2Ambiguous behavior of the enabled SubSystem55vii. . . . . . . . . . . . . . . .
List of Tables2.1Abstraction Levels of Software Languages, Directives, Utilities and Tools . .52.2SIGNAL Primitive Operators and Clock Relations . . . . . . . . . . . . . . .103.1SIMULINK Blocks Equations Using the BNF grammar . . . . . . . . . . . .184.1Typing Rules for Some SIMULINK blocks . . . . . . . . . . . . . . . . . . .244.2Type Inference Equations. Stavros Tripakis, Christos Sofronis, Paul Caspi,and Adrian Curic. Translating discretetime simulink to lustre. ACM Transactions on Embedded Computing Systems (TECS), 4(4):779818, 2005. Usedunder fair use, 2014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .25SIGNAL Primitive Operators and Clock Relations . . . . . . . . . . . . . . .294.3viii
Chapter 1IntroductionCyber Physical Systems (CPS) are engineering systems consisting of the integration of computational control and physical components with continuous dynamics. CPS are omnipresentin different sectors, such as agriculture, energy, transportation, building, healthcare andmanufactoring. As this systems are becoming more complex and their reliability, safety andcapability requirements are becoming more and more crucial, and harder to guarantee bythe traditional design tools and methodologies, new design paradigms are emerging.Model Based Design is a much discussed approach for developing such systems. It consists of building mathematical models that capture the specifications as well as the criticaldesign decisions for the system in the different stages of the development life cycle. The models have semantics derived from different theories such as finite state machines, tagged signalmodels [2], synchronous languages[3][4] and Metropolis meta models[5]. Different tools havebeen developed to generate correct by construction code from these models, as well as forthe verification of the system behavior in early design phases. Some of the most popular formal verification techniques for embedded software include model checking and abstraction.Model checking is used to exhaustively search through all behaviors of the finite abstraction.Abstraction is used to reduce the infinite state space systems into a finite ones.Despite the intensive research in the model based design, the Mathwork’s graphical environment SIMULINK[6] is still the most widely used tool for the design of embedded software.Although it is very convenient to use and easy to learn, SIMULINK does not have publishedand authentic formal semantics. Hence, its models can not be used with the Model BasedDesign framework. Its generated diagrams are verified through numerical simulation and itsbehavior is strongly correlated with the simulation configuration parameter. For example,switching from a fixed to a variable simulation step alters the output traces as well. Althoughsimulation based analysis is a well accepted technique in industrial practice, it becomes impossible to exhaustively simulate the system for verification purposes, once it gets verycomplex. Besides, little research work is done on quantifying the coverage obtained through1
Safa MessaoudChapter 1. Introduction2multiple simulations. SIMULINK has commercial code generators (Real-Time Workshopfrom Mathworks, TargetLink from dSpace). However, they have many restrictions. Forexample, TargetLink, does not generate code for blocks for the discrete Library. The preservation of semantic is another issue, since the behavior equivalence between the simulatedmodel and the generated code is unclear.Despite these limitations, SIMULINK remains a de-facto tool in the embedded control design for its convenience. Formal models, on the other hand, are less applied as they are lessintuitive to use and harder to learn. In order to close the gap between formal methods andindustrial practices, researcher have attempted to either give SIMULINK formal semantics[7]or translate it into formal models of computation[8][9][10]. In this thesis, we present a framework for translating discrete time SIMULINK models to SIGNAL[11] programs. SIGNAL isa data flow synchronous programming language which was developed by IRISA[12]. It doesnot assume the existence of any external trigger or global clock for reacting to the inputs.It is paced by the rate at which data arrives. Hence, each variable (Signal) within the software has its own clock, giving us the multi-rate (polychronous) formalism of SIGNAL. Thistiming model allows for streams to be computed asynchronously to one another which fitsvery easily to a multi thread environment. This increases the embedded software reactivityand capabilities. Moreover, a number of formal verification tools such as the model checkerSIGNALI[13] and the graphical developing interface SME[14] exist for Signal. These characteristics make SIGNAL an interesting model of computation for embedded software design.In this thesis, we develop a tool that only translate the discrete time blocks of SIMULINK.This choice is justified by the fact that, controller should be modeled as discrete time systems,so that they can be implemented on a computer.We follow the same translation methodologyproposed in [10], for translating LUSTRE to SIMULINK. The first two steps are clock inference and type inference. These steps provide us with information that will be needed in theatomic blocks translation and their hierarchical composition, while preserving the informalsemantics of SIMULINK, given by the behavior of the simulator. The preservation of semantics is checked by running with the same input sequence, both the SIMULINK simulation andthe corresponding SIGNAL program and obtaining in both cases the same output sequence.The novelty in this work consists of bridging the gap between the almost synchronous modelof computation of SIMULINK into a polychronous model of computation. In the past workby [10], the translation was straight forward due to the fact that the target language is synchronous and a global clock driven, whereas in SIGNAL language there is no global clock perse. A global clock may be calculated using the clock calculus if the translated SIMULINKmodel has the endochrony property. If a single global clock driver does not emerge, a polychronous model leading to multi-threaded behavior emerges. The other addition in this workis the use of affine clock relations between SIGNAL subprocesses when multiple SIMULINKblocks have sampled inputs with varying sampling rates but can be related by affine relations.The rest of the thesis is organized as follows: Chapter 2 is an overview of SIMULINK
Safa MessaoudChapter 1. Introduction3and SIGNAL formalisms. Chapter 3 is a survey of the translation of SIMULINK to differentmodels of computation. In Chapter 4, we present the translation framework. The resultsof applying our prototype tool on different SIMULINK models are shown in Chapter 5. Weclose this thesis with some concluding remarks and suggested future work.
Chapter 2Background2.1Model Based DesignFigure 2.1 shows a typical design cycle of an embedded system. Traditionally, engineers dealwith each stage of the process separately. Specification, design, coding, and testing are mostlydone independently. Engineers rely on design documents to provide the communicationbetween each of theses steps. This process suffers from a variety of drawbacks, including thedifficulty of keeping documentation updated. Another problem is that the coding processis often removed from the general design process. These are two issues where model-baseddesign can greatly improve the design process. Model Based Design consists of using Modelsof Computation that capture the specifications as well as the critical design decisions for thesystem in the different stages of the development life cycle. A Model of Computation (MoC)is defined as the manner in which computation and communication are being performed.Examples of MoC are Petri-Nets [15], Kahn Process Networks[16], synchronous languages(Esterel [3], Lustre[4]) and polychronous languages (SIGNAL).Model driven software design tools are based on using a high level language/Model of Computation, that are translated into a lower level language (C, RTL, etc.). The advantages of thisdesign methodology are two fold. Since the code generation is based on precise mathematicalmodels, this code is said to be correct-by-construction. Besides, the verification can be doneat higher levels of abstraction, which will reduce the costs, as well as the time to market.Table 2.1 gives an overview on the abstraction levels of the tools, programming languagesand their implementation paradigms. Properties of the synchronous and polychronous languages like reactivity, concurrency and deterministic execution fit the requirements of thesafety critical embedded software.4
Safa MessaoudChapter 2. Background5Figure 2.1: The V Design Process. http://www.engineering.com/DesignSoftware. Usedunder fair use, 2014Table 2.1: Abstraction Levels of Software Languages, Directives, Utilities and ToolsModel Driven ToolsLabVIEWSIMULINKPolychronyESTEREL StudioSCADE2.2Programming Languages Implementation LevelMATLABJavaESTERELRTLSIGNALC LUSTRECSIMULINKSIMULINK[6] is a computer-aided model driven design tool for embedded systems. It provides an interactive graphical environment and a customizable set of block libraries for thedesign, simulation, implementation, and test a variety of time-varying systems, includingcommunications, controls, signal, video and image processing. In SIMULINK, a system ishierarchically modeled using a set of blocks that are interconnected by ports. The blockscan be categorized into virtual and non virtual blocks. A virtual block only defines theinterconnections of signals and has no memory element. Examples of virtual blocks are themultiplexer Mux, Outputport and subsystems. Non virtual Blocks represent a set of equations, called block methods, which define a relation between the block inputs , outputs andthe state variables. Examples of non virtual blocks are Gain and Sum. The signals arethe communication conduits through which the blocks communicate with each others. We
Safa MessaoudChapter 2. Background6distinguish between data ports, defining data flow connection endpoints, and control ports,producing triggering or enabling events for the execution of subsystems. SIMULINK enablesto incorporate MATLAB algorithms into models and export simulation results to MATLABfor further analysis. SIMULINK has a multitude of semantics which depend on the userconfiguration. These semantics are only partially documented, mostly in natural language.The absence of formal semantics, makes the application of the static analysis techniquesineffective and restricts the verification of models to simulation based testing.2.3Synchronous Programming LanguagesIn order to better explain the motivation behind choosing SIGNAL for being the translation target language, we start by introducing the synchronous formalism. The essenceof synchronous model of computation is the synchrony hypothesis which assumes that thecomputation and communication time are instantaneous. In other words, time is organizedas a sequence of instants. In each instant, input events possibly occur, computation takeplace and control and data are propagated until an output is produced. This executioncycle at each instant is called a reaction. Hence, the history of a system is a totally orderedsequence of logical instants. Only the simultaneity or precedence between events matters.Thus, synchronous systems can be characterized by a global clock that acts as a referencefor each round of the input-output events. The global clock has no relation to the hardware clock, it only ticks at the different instants. This simple mathematical model makes iteasier to reason about the system, as it is deterministic (the output of the system entirelydepends on the inputs values and instants at which they occur) and predictable. Programsfor synchronous languages can be efficiently compiled into code for a finite state machinethat can be executed on a single processor. Although the synchrony assumption might seemunrealistic at the beginning, it can be easily validated in the implementation phase, on anactual execution platform on which the time of reactions is fully taken into account. Realtime constraints should be satisfied by the platform, so that satisfactory bounded delays ofthe reactions are ensured. Examples of synchronous languages are Lustre[4] and Esterel [3].2.4The Multi-rate Synchronous Language SIGNALSIGNAL is a declarative multi-rate synchronous language. While the synchronous languageshave a totally ordered model of
is motivated by its polychronous formalism that enhances synchronous programming with asynchronous concurrency, as well as, by the ability of its compiler of generating determin-istic multi thread code. Our translation involves three major steps: clock inferen
Introduction to Simulink Todd Atkins tatkins@mathworks.com. 4 Outline What is Simulink? Working with Simulink. How Simulink works. Continuous and discrete models Componentizing models. 5 Simulink Applications. 6 Simulink
Test Driven Development powered by MATLAB and Simulink 45 Model-Based Design –Simulink and Stateflow Manage Requirements –Simulink Requirements Author and Execute Tests –Simulink Test Measure Test Completeness –Simulink Coverage Refactor and Verify Compliance –Simulink Check
ES360 Introduction to Controls Engineering MATLAB and SIMULINK Help Page 2 of 6 Starting SIMULINK SIMULINK can be started by: 1) Opening a SIMULINK model file (model files use the .mdl extension). 2) Starting MATLAB and clicking on the icon in the tool bar. The SIMULINK Library Browser SIMULINK
Simulink and LEGO MINDSTORMS EV3 9 P a g e Project 1: Explore Simulink and LEGO MINDSTORMS EV3 P1.1 Get Started: Program EV3 Status Light with Simulink Motivation At the end of this project you will be able to program an EV3 brick from Simulink. Objective Create first model in Simulink Check hardware and software installation
Engineering POLYTECHNIC UNIVERSITY OF BARI Why Simulink? Simulink Real-Time (formerly known as xPC Target), together with x86-based real-time systems, is an environment for simulating and testing Simulink and Stateflow models in real-time on the physical system. Simulink easily allows to de
2.1 Sampling and discrete time systems 10 Discrete time systems are systems whose inputs and outputs are discrete time signals. Due to this interplay of continuous and discrete components, we can observe two discrete time systems in Figure 2, i.e., systems whose input and output are both discrete time signals.
Luigi Biagiotti Systems and Control Theory Introduction to Simulink-- 2 Simulink introduction Simulink (Simulation and Link) is an extension of MATLAB that offers modeling, simulation, and analysis of dynamical systems under a graphical user interface (GUI) environment. Simulink is based on block diagrams of Dynamic SystemsFile Size: 1MB
Introduction to Simulink 1.1 Objective The objective of Experiment #1 is to familiarize the students with simulation of power electronic circuits in Matlab/Simulink environment. Please follow the instructions in the laboratory manual. 1.2 Simulink Basics Tutorial Simulink is a graphical e
