Translating Discrete Time SIMULINK To SIGNAL

5m ago
30 Views
0 Downloads
788.93 KB
87 Pages
Transcription

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