Test Coverage • 𝑇𝑟𝑖𝑔𝑔𝑒𝑟𝑒𝑑 𝑚𝑜𝑑𝑒𝑠 𝑁𝑟. 𝑜𝑓 𝑚𝑜𝑑𝑒𝑠 % Inputs • Test Case • Model.mo OpenModelica • HDAE C-code Executable DAE1 DAE2 DAE3 Modes DAE1 DAE3 Modes Reduction DAE1 DAE2 DAE3 Triggered Modes  Test coverage of systems with continuous dynamics Master’s thesis in Systems, Control and Mechatronics. JAVIER GIL CEPEDA Department of Signals and Systems CHALMERS UNIVERSITY OF TECHNOLOGY Gothenburg, Sweden 2017 Master’s thesis 2017: EX002/2017 Test coverage for systems with continuous dynamics JAVIER GIL CEPEDA Department of Signals and Systems Division of Signals and Control Chalmers University of Technology Gothenburg, Sweden 2017 Test coverage for systems with continuous dynamics JAVIER GIL CEPEDA © JAVIER GIL CEPEDA, 2017. Supervisor: Sajed Miremadi, Volvo Car Corporation Examiner: Knut Åkesson, Department of Signals and Systems Master’s Thesis 2017:EX002/2017 Department of Signals and Systems Division of Signals and Control Chalmers University of Technology SE-412 96 Gothenburg Telephone +46 31 772 1000 Cover: Typeset in LATEX Gothenburg, Sweden 2017 iii Test coverage for systems with continuous dynamics JAVIER GIL CEPEDA Department of Signals and Systems Chalmers University of Technology Abstract Testing cyber-physical systems is a crucial part of the development process to en- sure correct operation. To determine how well a system is tested, this thesis pro- poses a novel methodology to measure test coverage for systems that contain both continuous and discrete dynamics. The approach is based on using the modelling language Modelica to obtain a mathematical representation of the behaviours of the system that can be translated to a hybrid automaton. Then, a metric called mode coverage is used to measure the exercised dynamical behaviours during the testing process. This work first describes mechatronic systems and how they can be modelled as hybrid automata, a case-study from the automotive industry is presented as an example. In a second stage, coverability criteria are presented as a metric to evaluate the quality of the test, and two strategies to perform test coverage are identified and analysed. Finally, a strategy based on structural analysis of modes is implemented to the case study and the proposed algorithm is described in detail. On the basis of the results, it can be concluded that the proposed methodology can be used to pinpoint dynamics that are not examined during the testing process. Such information can be further used to automate the generation of new test cases that trigger the unexplored regions. Keywords: Test coverage, mode coverage, hybrid automata, Model-Based Test- ing, Automation. iv Acknowledgements I would like to express my gratitude to all the people who contributed to the work described in this thesis. First of all, I thank my thesis advisor Dr. Knut Åkesson for engaging me in new ideas and guidance throughout the project. I would also like to thank my supervisor at Volvo, Dr. Sajed Miremadi for giving me this thesis opportunity but also supporting me to overcome problems that emerged during the thesis work. Finally, I would like to send my thanks out to Johan Eddeland for his clever and valuable insights. Javier Gil Cepeda, Gothenburg, January 2017 v Acronyms CPSs . . . . . . . . . . . . . . . . . . . Cyber-Physical Systems DAE . . . . . . . . . . . . . . . . . . . Differential Algebraic Equations GCOV . . . . . . . . . . . . . . . . . . GNU Coverage HA . . . . . . . . . . . . . . . . . . . . Hybrid Automata HDAE . . . . . . . . . . . . . . . . . . Hybrid Differential Algebraic Equations MBT . . . . . . . . . . . . . . . . . . . Model-Based Testing MC/DC . . . . . . . . . . . . . . . . . Modified Condition/Decision Coverage SMT . . . . . . . . . . . . . . . . . . . Satisfiability Modulo Theories SUT . . . . . . . . . . . . . . . . . . . . System Under Test vi Table of Contents Acronyms vi Contents vii List of Figures ix List of Tables x 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Purpose . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Research questions . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5 Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5.1 Justify research approach . . . . . . . . . . . . . . . . . . . 5 1.5.2 Research approach . . . . . . . . . . . . . . . . . . . . . . . 5 1.6 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2 Modelling Mechatronic Systems 7 2.1 Mechatronic Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Modelling fundamentals . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2.1 Modelling approaches . . . . . . . . . . . . . . . . . . . . . . 8 2.2.2 Hybrid DAE . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.2.1 Hybrid DAE in SimCode . . . . . . . . . . . . . . . 10 2.2.3 Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 Modelling Software . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3 Test Coverage for CPSs 15 3.1 Coverability criteria . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.1.1 The proposed criterion: mode coverage . . . . . . . . . . . . 16 3.2 Test coverage analysis: GCOV . . . . . . . . . . . . . . . . . . . . . 16 vii Table of Contents 3.2.1 Introduction to GCOV . . . . . . . . . . . . . . . . . . . . . 16 3.2.2 Methodology Workflow . . . . . . . . . . . . . . . . . . . . . 17 3.2.3 Analysis of C-code . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 Test coverage analysis: Hybrid Automaton . . . . . . . . . . . . . . 20 3.3.1 General algorithm . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3.2 Modes: from Hybrid DAE to Hybrid Automaton . . . . . . . 22 3.3.2.1 Identification of modes . . . . . . . . . . . . . . . . 23 3.3.3 Mode Reduction . . . . . . . . . . . . . . . . . . . . . . . . 27 3.3.3.1 Satisfiability Modulo Theories - the Z3 Solver . . . 27 3.3.3.2 Mode Reduction Workflow . . . . . . . . . . . . . . 28 4 Case study, Dog-Clutch 30 4.1 Description of the Dog-Clutch . . . . . . . . . . . . . . . . . . . . . 30 4.1.1 Modelling the Dog-Clutch . . . . . . . . . . . . . . . . . . . 31 4.2 Implementation and evaluation . . . . . . . . . . . . . . . . . . . . 33 5 Conclusion 37 5.1 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 5.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 A Clutch Model I B Hybrid DAE IV viii List of Figures 1.1 V-Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Model-Based Testing work-flow . . . . . . . . . . . . . . . . . . . . 3 1.3 Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1 Mechatronic system description . . . . . . . . . . . . . . . . . . . . 8 2.2 Causal modelling example . . . . . . . . . . . . . . . . . . . . . . . 8 2.3 Acausal modelling example . . . . . . . . . . . . . . . . . . . . . . . 9 2.4 DAE example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.5 Hybrid automaton . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.6 OpenModelica compiler stages . . . . . . . . . . . . . . . . . . . . . 14 3.1 GCOV workflow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.2 C-code from OpenModelica . . . . . . . . . . . . . . . . . . . . . . 19 3.3 GCOV results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.4 Approach to measure test coverage . . . . . . . . . . . . . . . . . . 20 3.5 Algorithm to find triggered modes . . . . . . . . . . . . . . . . . . . 22 3.6 Hybrid automaton . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.7 Z3 Satisfiability example . . . . . . . . . . . . . . . . . . . . . . . . 27 3.8 Mode reduction algorithm . . . . . . . . . . . . . . . . . . . . . . . 28 3.9 Example of the mode reduction algorithm . . . . . . . . . . . . . . 29 4.1 Dog-clutch operation . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.2 Dog-Clutch model . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.3 Distance limits in the clutch model . . . . . . . . . . . . . . . . . . 32 4.4 Result Test Coverage . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ix List of Tables 2.1 DAEs generated by conditional equations . . . . . . . . . . . . . . . 11 2.2 Hybrid DAE generated for the case study . . . . . . . . . . . . . . . 12 3.1 Modes description . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.1 Conditions from Appendix B . . . . . . . . . . . . . . . . . . . . . . 33 4.2 Parsed conditions: Case study . . . . . . . . . . . . . . . . . . . . . 35 4.3 Modes in the case study . . . . . . . . . . . . . . . . . . . . . . . . 36 x 1 Introduction Test Coverage is a measure extensively used in software engineering to charac- terise how well a model is tested. This thesis provides a definition of test coverage for systems with continuous dynamics and develops an algorithm to measure test coverage. The algorithm has been evaluated on a use case from Volvo Car Corpo- ration. This master’s thesis is a part of TESTRON [1] project carried out by Chalmers University of Technology, Volvo Car Corporation and Quviq AB and funded by VINNOVA, the Sweden Innovation Agency. 1.1 Background Cyber-Physical Systems (CPSs) [2] [3] are closed loop feedback systems that present high interconnection between the physical world and one or more com- puting devices. As the level of capacity of computation has been increasing along the years, more and more physical systems, such as biological systems, smart grids or communications have started to be regulated by means of controllers. These devices perform tasks such as computation or communication through sensors and actuators, reacting in real time to the environment. Cyber-physical systems are today ubiquitous in many different areas, such as transportation, robotics, health care, energy, military or communication. Applications of CPSs with a high level of inherent risk associated may be called safety-critical and must, thus, be handled with special attention. These systems have as their first requirement the correct (safe) operation rather than cost or performance. Examples of safety critical applications are: a cruise controller in a car, electronic medical equipment and the autopilot in an aeroplane. Thus, an exhaustive analysis and verification of these systems is of crucial importance. Verification can be defined as the process of determining whether a model meets the specified requirements, ensuring that the system is well-engineered. In the industry, the most common process to verify a model is by testing. Historically, experienced engineers with high knowledge about the system under test did veri- 1 1. Introduction fication by manual testing. Yet, the actual level of complexity acquired by CPSs and the increased number and detail of specifications make it hard and, in prac- tice, impossible to manually verify these kind of systems. Most important, the continuous increment of costs motivates new testing approaches in the industry to automate testing processes. One emerging novel technique that will be implemented in the TESTRON project, which has drawn attention in the past decade, is Model-Based Testing (MBT) [4]. This approach is growing importantly in the automotive industry due to the tendency towards the use of the Model-Based Design (MBD) methodology in the development of embedded software, above all to comply with ISO26262 "Road vehicles – Functional safety" [5]. The advantage of the MBT approach is that errors can be detected and fixed already in the early design phases, instead of in integration or marketing stages as is shown in Figure 1.1. Saving costs and facil- itating faster developments are important improvements achieved with the MBT implementation [6]. Requirements Design Code Integration User acceptance Model-Based Testing Figure 1.1 – Model-Based Design process. Model-based testing is implemented in the earlier stages of the development process. From D. Firesmith [7]. The overall structure of the MBT technique is presented In Figure 1.2. The motivation of this work lies in the last step of the algorithm where testing quality is evaluated. A test script automates a process where a test case is executed on a System Under Test (SUT) and finally a verdict is assigned to each test case. The question that arises now is how test quality can be measured to generate a verdict. A common method used in software testing is test coverage. Yet, typical cover- age criteria for structural analysis at code level as Modified Condition/Decision Coverage (MC/DC) have been questioned in [8] using a simple example of CPSs. This is because analysis for verification of CPSs models is in general complex due to the interaction between continuous and discrete dynamics. 2 1. Introduction When talking about MBT, the importance of the coverage criterion is not limited to providing a metric to measure test quality. In fact, the objective of test coverage is to find areas that have not been covered by the test cases. The test criterion serves therefore as a guideline in the generation of new test cases to cover such areas. Another important property is that it may be a useful input to a test- stopping rule. When the criterion is fulfilled or it has been reached an acceptable level of coverage the testing may be stopped. Adaptor + Env Test Selection Criteria Requirements Test Case Specification Model Verdicts Test Cases Test Script (1) (2) (3) (4)(4) (5!2) (5!1) SUT Figure 1.2 – Model-Based Testing work-flow from [4]. This master’s thesis focuses in the last steps, 5-1 and 5-2. A test script is used to execute a test case on a SUT and as a result a verdict is achieved. The aim of this master’s thesis is twofold. Firstly, to define a coverage criterion suitable for CPSs which answers the question, “What property of a CPSs must be tested” Secondly, develop an algorithm to evaluate how well a test case tests the property defined by the coverage criterion and returns a verdict. For the first question, mode coverage criterion is used because it fits better with CPSs. Regarding the second question, the algorithm proposed translates cyber-physical systems into Hybrid Automata (HA) [9] [10] to be used for analysing test coverage. 3 1. Introduction 1.2 Purpose The purpose of this thesis is to create a tool that measures test coverage for a system with continuous dynamics. To that end, an algorithm has been developed and implemented that takes as inputs a system under test (SUT) and a test case(s) and returns the test coverage according to a pre-defined criterion. 1.3 Related Work Hybrid systems have been extensively studied in the literature, in Alur R. et al. [9] the framework of hybrid automata (HA) is introduced to verify linear hybrid systems. Henzinger T. [11] applies model-checking techniques in HA for formal verification concluding that reachability is undecidable even for simple hybrid au- tomata. Regarding test coverage for hybrid systems two approaches have been reviewed. In A. Agung Julius et al. [12], the infinite set of possible testing scenarios is reduced to a finite set by means of the notion of robust neighbourhoods. The testing aims to cover all these finite scenarios. In the work presented by Tarik Nahhal and Thao Dang [13] the coverage criterion used is state coverage. The state space is divided into regions with the same characteristics and the notion of star-discrepancy is used to describe how well the visited states represent the reachable set of the system. The objective is to test the state space as much as possible without leaving big unexplored areas. This method faces the problem of the infiniteness of states in complex models, which requires a very long time of computation and have no measure of that all modes have been tested. As a difference, the algorithm proposed in this master’s thesis calculates test coverage by reducing the infinite state space to a finite set of modes. Such modes are used as a coverage criterion to quantify test coverage. Another difference is that while previous works use hybrid automata to represent hybrid systems, neither of them describes the process to generate it. The algorithm presented here establishes a method to automate the creation of a hybrid automaton to be used in the testing process. The increasing attention and resources laid on the verification of hybrid systems are reflected in the rising number of developed tools using MBT techniques. On one hand, Reactis Tester and TestWeaver are testing and validation tools that try to maximise the degree of coverage by using guided simulation techniques [14]. On the other hand, Simulink Design Verifier uses formal methods and SAT-solving techniques to automatically generate test cases for state coverage [15]. The tool developed in this master’s thesis does not use formal methods to verify a model and differs from the other approaches in that, mode coverage is used instead of 4 1. Introduction state coverage as a metric to evaluate test coverage. 1.4 Research questions The following questions are answered in this thesis: RQ1: What coverage criteria for hybrid systems are useful for testing? RQ2: How can modelling languages as Modelica, be transformed into mathemati- cal descriptions suitable for analysis? RQ3: What are the strength and weakness of the proposed coverage criteria? 1.5 Method This subsection firstly justifies the qualitative approach followed throughout this thesis with the aim of answering the research questions defined in the previous chapter. Secondly, the approach is presented. 1.5.1 Justify research approach 1. The acausal modelling approach was used as it efficiently models CPSs and is able to translate them into a mathematical representation. Among all the modelling environments, OpenModelica was chosen since it allows control over all the processes, from model description to the simulation. 2. Hybrid automata is a well studied formal model, suitable to be applied in the analysis of hybrid systems. Research and programming development was carried out to achieve a systematic way to generate hybrid automata from a mathematical description provided by OpenModelica. 3. Two different coverage criteria were studied resulting in mode coverage as a criterion to quantitatively measure test coverage. 4. The approach followed along the thesis allows exploiting the advantages of emerging satisfiability modulo theories solvers to efficiently reduce the num- ber of unreachable modes in the HA. 1.5.2 Research approach The aim of the thesis is to measure test coverage for systems with continuous dynamics. The approach followed can be summarised in Figure 1.3. A CPS system is represented by the control and plant blocks and the feedback loop. The control block describes the discrete dynamics while the plant describes the continuous 5 1. Introduction dynamics. Thus, the goal is to find the dynamical behaviours or modes of the plant block that are excited by a test vector. Control Plant Test vector Modes Figure 1.3 – The method followed in this thesis aims to identify modes that are triggered by a test case in a cyber-physical system. The modes describe continuous dynamics in the plant block. The procedure followed is described below: 1. The modelling framework OpenModelica was used to transform a CPSs sys- tem described in Modelica language into a hybrid DAE. After analysing the results obtained from OpenModelica, it was decided to use a hybrid automata as the system from which to measure test coverage, also mode coverage was identified as a proper coverage criterion since it is particularly useful in analysing hybrid automata. 2. The hybrid DAE was used to automatically generate a hybrid automaton, which is a mathematical description suitable for test coverage analysis. 3. By using the Z3 solver, the HA was reduced removing the unfeasible modes. 4. Measure test coverage with mode coverage as a criterion. 5. Throughout the process, strength and weakness of the approach were exam- ined. The application developed has been implemented in Python and two software tools have been used, OpenModelica and the Satisfiability Modulo Theories (SMT) Z3 solver. 1.6 Contributions To the best knowledge of the authors, this master’s thesis proposes a novel method- ology to perform test coverage based on the use of the Modelica language to repre- sent CPSs as hybrid automata. Furthermore, it is proposed the definition of mode coverage as a coverage criterion to determine how well a system is tested. 6 2 Modelling Mechatronic Systems Modelling mechatronic systems consist of capturing the dynamics of a system in a mathematical description. Among all the possible representations, two are of particular importance for this work: the Hybrid Differential Algebraic Equations (HDAE) and the hybrid automata. This chapter is organised as follows: Mechatronic systems are first presented to later move on towards modelling concepts as modelling approaches, mathematical representations and different software for modelling and simulation mechatronic systems. Finally, the Dog-Clutch model used through the thesis is presented. 2.1 Mechatronic Systems Mechatronic systems are a type of cyber-physical systems where the physical part is a mechanical system. An outline of a mechatronic system is presented in Figure 2.1. Typically, a micro-controller running a control algorithm is located in the electronic domain. On the other side, a robot or some mechanical process interacting with the environment is used in the mechanical domain. The communication between the two domains is conducted through actuators to perform the actions decided by the controller and through sensors providing the feedback from the mechanical part. Examples of mechatronic devices are robots and manipulator arms, more complex examples are aeroplanes. The mechatronic system investigated here is a dog-clutch that is explained in detail in section 4. This device is used to propagate motion by coupling two rotating shafts. 2.2 Modelling fundamentals This section describes the two mathematical representations used throughout the modelling process, the hybrid DAE and hybrid automata. The objective is to translate the original model coded in Modelica into hybrid automata, which is a suitable structure to analyse test coverage, a HDAE is used as an intermediate step. 7 2. Modelling Mechatronic Systems Control Algorithm Actuators Sensors Process Electronics Mechanics Figure 2.1 – Description of the interaction between the electrical and the me- chanical part of a mechatronic system 2.2.1 Modelling approaches A mechatronic system usually consists of two parts: a controller and a plant. Modelling the controller usually includes sensors and actuators and may experience jitter, delay times and other disturbances. Since control algorithms are designed using a model of the plant, it is thus necessary to model the mechanical system as close as possible to the reality. The implementation of the plant is a difficult task due to the highly complex interaction between the different domains. Two prominent approaches are commonly used to carry out modelling tasks, causal and acausal modelling, both are described below in more details. Figure 2.2 – Simulink model of an inductor where the input is the voltage and the output the current 1. Causal modelling: Causal models follow the principle of causality. Blocks have defined inputs and outputs that impose a causal relationship between variables. The interconnection between different blocks is done by links, 8 2. Modelling Mechatronic Systems which transmit signals at each time step. The model is constructed follow- ing the dependencies between variables, generating a determined data flow direction for the signals. Systems that present such behaviour are called causal systems, an example of this is created with Simulink and shown in Figure 2.2, where a mathematical description of an inductor is used to ob- tain current from a voltage input. One disadvantage of this approach is that the model diagram follows a hierarchy and represents the mathematical re- lationships rather than the physical representation of the model. Another drawback is the re-usability of the block, in this case, it can only be used to compute current when the voltage and resistnce are given. 2. Acausal modelling: This approach also called the Physical Network Ap- proach aims to model physical systems through a mathematical description made up by a set of Differential Algebraic Equations (DAE). Unlike the causal approach, equations neither specify input nor output variables. In this context, equations must be understood as relations among variables, not as assignments, therefore causality is not specified. The directionality or data flow of the variables among blocks is defined during simulation time when the equations are solved. Graphically the acausal approach provides a model with a topology very similar to the real physical model. Figure 2.3 describes a simple example where an ideal inductor is created. The icon represents an inductor that is governed by the relation L · di dt = V , where voltage and current flows are simultaneously simulated. 1 model Inductor "Ideal linear electrical inductor " 2 extends Interfaces.OnePort (i(start =0)); 3 parameter SI.Inductance L(start =1) " Inductance "; 4 equation 5 L*der(i) = v; 6 end Inductor ; Figure 2.3 – A script that models an Inductor using Modelica is shown within the frame. Above the script, the graphical representation of the class Inductor is depicted. The second approach, acausal modelling, fits better with the aim of this thesis in the sense that it is possible to extract the equations describing the behaviours 9 2. Modelling Mechatronic Systems of the model to analyse it. That is in opposition to the causal approach, where only a bunch of C-code files is obtained making it complicated, if not impossible, to analyse behaviours of mechatronic systems. In fact, the equations provided by acausal modelling are expressed in a structure called hybrid DAE that is described more exhaustively in the next section. 2.2.2 Hybrid DAE A hybrid DAE can be summarised as a mathematical model that switches its behaviour with time and is composed of a set of DAEs, representing continuous dynamics. Below are briefly introduced, from a less to a more complex level, the different systems of equations that define a hybrid DAE. An example of how a HDAE looks is presented in Figure 2.4. Algebraic equations describe the design and physical constraints among vari- ables. It does not contain derivatives of the system variables. Ordinary differential equations are equations with derivatives that models rates of change of the system variables and are used to describe natural phenomena. Differential algebraic equations are a generalization of ODE’s including alge- braical equations. A DAE can be expressed as F (ẋ, x, t) = 0. ẋ1 = 2x1 + u1 ẋ2 = 4x2 + 6u2 } ẋ = f (x, u) Differential equations x1 = 3x2 h(x) = 0 Algebraical equation Figure 2.4 – Example of a DAE composed by two differential equations and one algebraical equation. Hybrid DAEs naturally arise during the modelling process of physical systems. This mathematical description is the tool used to construct hybrid automata from which test coverage will be analysed. 2.2.2.1 Hybrid DAE in SimCode As far, the concept of hybrid DAE has been introduced without any mention with regard to its implementation in a computational language. An efficient way to represent HDAEs is through conditional equations also called if-equations, an example of two conditional equations is shown in (2.1). In this simple example, the value of the variables a and b defines the expression at which variables ẋ and 10 2. Modelling Mechatronic Systems x are updated. The two conditional equations describes four different DAEs that are shown in Table 2.1. ẋ1 = { 2x1 + u, if a < 0 −(x1 + u), if a ≥ 0 (2.1a) x2 = { 1, if b < 0 0, if b ≥ 0 (2.1b) a, b < 0 ẋ1 = 2x1 + u x2 = 1 ẋ1 = 2x1 + u x2 = 0 a < 0; b ≥ 0 a ≥ 0; b < 0 ẋ1 = −(x1 + u) x2 = 1 ẋ1 = −(x1 + u) x2 = 0 a, b > 0 Table 2.1 – DAEs generated by the conditional equations in (2.1). The modelling software OpenModelica uses the hybrid DAE mathematical de- scription to collect all the information related to the dynamics of the model in a data structure called SimCode. A simplified version of the SimCode for the case study is shown in Table 2.21. The different DAEs that conforms the hybrid DAE are described by regular equations and the conditional equations (2.2a), (2.2d), (2.2e) and (2.2f). The variables defined by if-equations, update its value according to the guards Gi that are evaluated to true or false each time instant. 2.2.3 Hybrid Automata A hybrid automaton is a high-level formal model that can be described as an extended finite automata (EFA) with continuous state variables. EFAs are usually modelled using modes, edges and guards. In this thesis a mode represent a discrete region or location in a graph that determines a specific continuous dynamic of the plant. Edges and guards are used to represent the transitions between modes. A HA can evolve in two different ways, by discrete and by continuous evolu- tion. In the first case, a transition is satisfied bringing the system to a new mode and imposing a different behaviour. In the second case, continuous state variables 1For the sake of clarity some equations have been reduced 11 2. Modelling Mechatronic Systems engage_req = if G1 then 1 else 0 (2.2a) f_spring_current = KI * current + (-k_spring) * z - DampingBelleville * zv (2.2b) a = 0.02777777777777778 * sin(36.0 * phi) (2.2c) $DER.zv = if G2 then if G3 then DIVISION(f_spring_n_current, mass) else (2.2d) DIVISION(f_spring_n_current - stiff2 * (-0.0016 + z), mass) else 1 t = if G4 then if G5 then 2 else if G6 then HiSpeed2 * w else 1.5 else 0.0 (2.2e) eng_state = if G7 then if G8 then 0.0 else if C9 then 1 else 0.0 else 0.0 (2.2f) $DER.z = zv (2.2g) $DER.phi = w (2.2h) prev_eng_state = pre(eng_state) (2.2i) Table 2.2 – Set of equations and conditional equations that included in a hybrid DAE in OpenModelica. The guards Gi are evaluated to true or false at each time instant. evolve according to differential algebraic equations. For mechatronic systems the controller determines the locations of the EFA and the mechanical system deter- mines the continuous dynamics. A more formal definition of Hybrid automaton is presented below: Definition 2.1. Hybrid automaton [9] [13]: A Hybrid automaton is defined by a five-tuple as: 〈X ,Q,F , E ,G〉 (2.3) X ⊆ Rn is the continuous state space of the system in which continuous state variables are defined. Here X ⊆ Rn Q = 〈q1, q2, ..., qn〉, n ∈ N is the finite set of modes or regions. Discrete transi- tions switch between different behaviours. Associated with each mode is a DAE describing the behaviour (dynamics) of the system. F : X ×Q → X represents the vector field that defines the continuous dynamics in each mode. In this work continuous dynamics are described by DAEs. E ⊆ Q × Q is a finite set of edges representing discrete transitions. A transition e ∈ E is defined by a three tuple (m, m′, g) where m is the origin mode, m′ is the target mode and g ∈ G is the guard of the transition. Transitions determines the discrete dynamics. G : Ge|e ∈ E is the set of guards enabling transitions among different modes. When a guard is evaluated to true, a new mode becomes active imposing a new behaviour. In this report, guards are represented by predicates. Definition 2.2. Hybrid State 12 2. Modelling Mechatronic Systems (q, x) ∈ Q × X is a specific hybrid state of the system which includes discrete and continuous variables. G𝑢𝑎𝑟𝑑 1 ? G𝑢𝑎𝑟𝑑 2 ? 𝑥1 = 2𝑥1 + 𝑢1 𝑥2 = 4𝑥2 + 6𝑢2 𝑥1 = 3𝑥2 𝑀𝑜𝑑𝑒 1 𝑀𝑜𝑑𝑒 2 𝑥1 = 𝑥1 + 2𝑢1 𝑥2 = −𝑥2 + 𝑢2 3𝑥1 = 𝑥2 Figure 2.5 – Hybrid Automaton with two modes. Transitions between modes are enabled when the corresponding guard is evaluated to True. At each mode a DAE defines the dynamics of the system. 2.3 Modelling Software To carry out the modelling task there are plenty of commercial software avail- able. Below, the modelling environments considered during this project are briefly presented. • Causal Approach: Simulink®: is a block diagram environment for multidomain simulation and Model-Based Design [16]. • Acausal approach: Simscape™: is a tool for modelling and simulating multidomain physical systems. [17]. This is the tool used at Volvo Car Corporation to imple- ment the dog-clutch model, this model is discussed later in this report. OpenModelica: is an open-source Modelica-based modelling and simula- tion environment intended for industrial usage [18]. In this thesis Open- Modelica was selected to carry out the simulation process. The decision towards using OpenModelica as the modelling environment was motivated by two qualitative criteria. Mainly because it uses an acausal modelling 13 2. Modelling Mechatronic Systems approach so that dynamics are described by equations. The other important reason is that OpenModelica provides an open source environment where it is possible to rewrite the internal code and customise all the internal steps involved in the simulation process. This property was really appreciated in the beginning of this work because it gave great versatility to decide among different strategies in order to answer the proposed research questions. For instance, one of the first issues was about to choose between the generated C-code files or the optimised sorted equations to identify the different modes or behaviours of the system. CHAPTER 2. BACKGROUND 2.4. OPENMODELICA COMPILER (OMC) that will not change at runtime). Another reason that the code optimizer is often found towards the end of the transformation chain is so that it can perform machine dependent optimizations: for example use special assembly instructions only available on certain processors. Finally the optimized intermediate code is translated to the target program in the code generator. If the target program is written in machine code you can execute it right away. But if the target program is written in C for example you have to compile it with a C compiler to obtain an executable. 2.4 OpenModelica Compiler (OMC) The OpenModelica Compiler (OMC) is the core of the OpenModelica environment [5]. Its main job is to translate Modelica code to C code. The generated C code has to be compiled with a C compiler and linked together with runtime and simulation libraries to produce the final result. In addition to processing files on the command line, OMC can also be started as a background pro- cess and will then accept commands from other processes such as the interactive shell (Figure 2.3). The translation process from Modelica code to executable code is depicted in Figure 2.7. Figure 2.7 Compiler phases in the OpenModelica compiler (taken from [5]). Modelica Source Code Translator Analyzer Optimizer Code Generator C Compiler Simulation Modelica model Flat Model Sorted equations Optimized sorted equations C Code Executable First the Modelica source code is parsed into a parse tree similar to the one in Figure 2.6. The trans- lator phase converts this parse tree to a so called flat model. In the flat model the code has been type- checked, all object-oriented operations have been performed, and definitions from external packages have been included. The flat model only consists of equations, declarations, and functions. The next two phases, the analyzer and optimizer, are necessary for compiling equations. They ma- nipulate and simplify the equations so that they are on a form suitable for solving numerically. Finally C code is generated that is compiled with a C compiler and linked together with runtime and simulation libraries. The compiler is divided into a set of modules depicted in Figure 2.8. Since this thesis deals only with the code generation phase of OMC, the most important modules are CodeGen and SimCodeGen (located in the right middle in the figure). CodeGen translates functions to C code and SimCodeGen deals with equations. 7 Figure 2.6 – OpenModelica Compiler Translation stages from Modelica code to executable C-code. Figure taken from P. Fritzson et al. [19]. The workflow of OpenModelica is summarised in Figure 2.6. OpenModelica takes as input a model described in the Modelica language and after some internal steps, the model is translated to a structure with optimised equations. This struc- ture is internally called SimCode and is the object used to generate the C-code for simulation. The importance of this structure lies in the fact that the set of equations describe a hybrid DAE which can be dumped into a file or read from the C-file. 14 3 Test Coverage for CPSs Two different approaches to perform test coverage are presented in this section. The first is structural analysis of the code and the second is structural analysis of the modes. After evaluation of the two different options, the second approach was chosen. Finally, the general algorithm is presented to check test coverage using a model and a test case. 3.1 Coverability criteria As previously mentioned in the introduction, verification is used to assure the correctness and can be done in a variety of ways. However, testing is the most common process to verify a model. A common method used by software engineers to evaluate the quality of testing is test coverage analysis. Test coverage is a technique used within software testing to quantify the degree to which a model is covered during the testing process. Using this technique requires, above all, to decide what property or characteristic of the system should be measured. An adequate metric or coverage criterion has to be defined indicating what properties must be exercised to perform a “good” test. Based upon a chosen metric, it is possible to quantify how well the SUT is explored under simulation. For instance, statement coverage is a typical coverage criterion in the industry, which describe whether a statement of a code have been executed at least once or not at all. The degree of compliance reached during testing can be measured quantitatively by the percentage of statements executed. According to [20], many development standards claim structural coverage cri- teria at code level as the best practice in industrial software development. Such types of criteria aim to analyse the structure of the program. Some examples of those criteria are: function coverage, statement coverage, branch coverage and condition coverage [21]. Unfortunately, these criteria do not fit well with CPSs. CPSs are non-deterministic reactive systems i.e. they constantly interact with its environment in a manner that one input to the system can lead to different outputs depending on the state of the environment. This is in opposition to the 15 3. Test Coverage for CPSs classical model of computation where for one input a specific output is expected. In [8], it has been shown that the coverage criterion Modified Condition/Decision Coverage (MC/DC) is not able to exercise all the modes of an elementary case of CPSs even if the MC/DC coverage is fulfilled. Thus, classical software test criteria are inadequate for verification of CPSs. Other coverage metrics as state coverage have been used [13] to measure test coverage for CPSs. Though, CPSs have continuous states implying that the state space is infinite so that in practice it cannot be entirely explored. Other appropri- ate coverage criteria should be used. 3.1.1 The proposed criterion: mode coverage The objective of this master’s thesis is to cover/excite all the different finite be- haviours of the system. Based on this idea, two coverability approaches have been identified and examined. The first approach studied was structural analysis at code level that involves the GNU Coverage (GCOV) tool. The second approach is intended for structural analysis of modes1 and requires the use of hybrid automata and Satisfiability Modulo Theories (SMT). After having examined the two methods, the proposed criterion was mode cov- erage and is defined as follows: Mode Coverage = Number of modes exercised during simulation set of reachable modes × 100% (3.1) In the next sections both approaches to do test coverage are described thor- oughly. 3.2 Test coverage analysis: GCOV This part presents the approach followed towards accomplishing test coverage at code level. To begin with, the GCOV tool is introduced and later the method- ology used to analyse C-code for test coverage is explained. To conclude, the disadvantages that led to discarding this approach are explained. 3.2.1 Introduction to GCOV GCOV [22] is a software tool for coverage analysis of code generated by the GCC compiler (GNU Compiler Collection). This is the compiler used by OpenModelica to generate the C-code for simulation. For the goal of this thesis, the interesting 1The definition of mode is in 2.1 16 3. Test Coverage for CPSs functionality of this tool is its ability to count lines of code that are executed during simulation. 3.2.2 Methodology Workflow The workflow of the method followed is summarized in Figure 3.1. Since it was decided to use OpenModelica, a manual translation from Simscape code to Mod- elica code was done. Inside OpenModelica a SimCode structure, that contains all the information needed for C-code generation, was generated. SimCode is later passed as input to a process where C-code files are returned. The last step lies in executing the GCOV tool upon the C-code to obtain structural coverage analysis at code level. Manual Translation OpenModelica GCOV Figure 3.1 – Work-flow followed to perform structural coverage analysis at code level employing GCOV. The attractive point of this methodology is that dynamics described by equations in the original model are captured by the C-code. Another advantage is that OpenModelica tracks all the processes of equation transformations in such a way that C-code can be easily interpreted and hence, analysed. 3.2.3 Analysis of C-code The aim of the analysis is to identify, in the C-code, all behaviours of the system triggered during simulation. It is useful to recall that behaviours are described by DAEs which, in turn, are made up of set of equations, as it is shown in section 2.2.2. The algorithm to perform test coverage is summarised in three steps below: 1) to identify lines where the equations that defines dynamics are located. 2) to check whether those lines have been triggered or not. 3) calculate the percentage of equation triggered against the total number of equations The C-code generated2 from the conditional equation (2.1a) is used in Figure 3.2 to exemplify how the analysis has been carried out. The highlighted lines 13 2For the sake of clarity the code has been slightly modified 17 3. Test Coverage for CPSs and 17 assign one of the two dynamics to the variable tmp2, which value is later updated to the variable ẋ in line 19. Identification of lines that assign dynamics was done using the libClang [23] package inside the programming environment Eclipse. LibClang parses the source code generating an abstract syntax tree that can be traversed later to find specific parts of the code. GCOV was invoked to identify whether lines were executed during simulation or not. When GCOV completed the analysis, it was returned a file containing, among other information, the times a line was executed. In Figure 3.2 can be seen that both lines 13 and 17 were executed at least one time. In particular, 8808 and 6677 times respectively. In this case, test coverage would be 100% as both behaviours of the variable ẋ were exercised. Several drawbacks were found during the implementation that makes difficult to follow this approach. The most important are listed below: • This method allows to account how many times the different equations that defines the dynamics are triggered during simulation but is not capable of discerning which of them are triggered concurrently. That is important be- cause the combination of the dynamics is what defines the behaviour or mode at any given moment. As a result it is not possible to identify modes with the GCOV solution proposed. • The method to detect specific lines in the C-code lacks generality. Actually, parsing C-files could be a complex task if the objective is to automate the process to all possible models. • It is necessary to modify the OpenModelica compiler to generate C-code files with a suitable format for GCOV. Some necessary modifications are: to remove the use of the C ternary operator “?”, to handle different types of linear and non-linear functions to make them explicit, modify the makefile that compiles and links the C-code, etc. Although these adjustments can be done, it could be a source of frequently occurred problems. Before this method was implemented, and due to the aforementioned disadvan- tages, it was decided to move on with another approach that is discussed in the next section. 18 3. Test Coverage for CPSs 1 /∗ 2 equat ion index : 15 3 type : SIMPLE_ASSIGN 4 der(x) = if a < 0 then 2x + u else -(x + u) 5 ∗/ 6 void clutch_eqFunction_15 (DATA ∗data , threadData_t ∗ threadData ) 7 { 8 const i n t equat ionIndexes [ 2 ] = {1 ,15} ; 9 RELATIONHYSTERESIS(tmp0 , $Pa , 0 , 0 , Less ) ; 10 tmp1 = ( modelica_boolean ) tmp0 ; 11 i f ( tmp1) 12 { 13 tmp2 = (2) * (x + u); 14 } 15 e l s e 16 { 17 tmp2 = (-1) * (x + u); 18 } 19 DER(x) = tmp2; 20 } Figure 3.2 – Script showing the C-code generated from the conditional equation in (2.1a). Highlighted lines show the conditional equation in Modelica language and the sentences where the script assigns dynamics to the variable ẋ 1 −: 1 : /∗ 2 −: 2 : equat ion index : 15 3 −: 3 : type : SIMPLE_ASSIGN 4 −: 4 : der(x) = if a < 0 then 2x + u else -(x + u) 5 −: 5 : ∗/ 6 15485 : 6 : void clutch_eqFunction_15 (DATA ∗data , threadData_t ∗ threadData ) 7 −: 7 : { 8 −: 8 : const i n t equat ionIndexes [ 2 ] = {1 ,15} ; 9 15485 : 9 : RELATIONHYSTERESIS(tmp0 , $Pa , 0 , 0 , Less ) ; 10 15485 : 10 : tmp1 = ( modelica_boolean ) tmp0 ; 11 15485 : 11 : i f ( tmp1) 12 −: 12 : { 13 8808 : 13 : tmp2 = (2) * (x + u); 14 −: 14 : } 15 −: 15 : e l s e 16 −: 16 : { 17 6677 : 17 : tmp2 = (-1) * (x + u); 18 −: 18 : } 19 15485 : 19 : DER(x) = tmp2; 20 15485 : 20 :} Figure 3.3 – Example of the file generated by GCOV where the script in Figure 3.2 is the input. It shows how often each line is executed during simulation. Highlighted lines show the conditional equation in Modelica language and the sentences where the script assigns dynamics to the variable ẋ 19 3. Test Coverage for CPSs 3.3 Test coverage analysis: Hybrid Automaton A hybrid automaton is a formal model that may be used to analyse CPSs because of its ability to reduce the infinite state space to a finite set of locations called modes, this property provides a new coverage criterion calledmode coverage. In the course of this section is described the approach followed to perform test coverage as proposed in (3.1). Initially, the general algorithm to quantify mode coverage is presented, then, two steps of the algorithm are described in more detail: the abstraction from a hybrid DAE to hybrid automata and the operation of the Z3 Solver to reduce the number of modes in a HA. 3.3.1 General algorithm The algorithm developed during this master’s thesis to automate the process of quantifying test coverage for CPSs is hereby presented, see Figure 3.4. The ap- proach taken is based on the translation of a hybrid DAE to a formal model described as a hybrid automaton. Then, test coverage is carried out aiming to exercise all the modes of the system, the different steps are described below. Test Coverage • 𝑇𝑟𝑖𝑔𝑔𝑒𝑟𝑒𝑑 𝑚𝑜𝑑𝑒𝑠 𝑁𝑟. 𝑜𝑓 𝑚𝑜𝑑𝑒𝑠 % Inputs • Test Case • Model.mo OpenModelica • HDAE C-code Executable DAE1 DAE2 DAE3 Modes DAE1 DAE3 Modes Reduction DAE1 DAE2 DAE3 Triggered Modes  Figure 3.4 – Overview of the approach followed to perform test coverage starting from a test case and a model of a CPSs described in Modelica language. • Inputs: The algorithm begins with a model to be tested and a test case to excite behaviours of the model. 20 3. Test Coverage for CPSs • OpenModelica: The environment OpenModelica takes the model.mo and generates a hybrid DAE that is saved in a data structure named SimCode from which modes can be extracted to generate a hybrid automaton. The second input, the test case, and an executable file are used in the last step to simulate the original model. The results of the simulation are saved in a file that is later on used to identify the triggered modes during simulation. The most importance of using OpenModelica resides in the fact that it was transformed a Cyber-Physical system into a Hybrid DAE. • Modes: A hybrid automaton is created from a hybrid DAE. At this step, all feasible and infeasible modes are identified. This process is explained in detail in section 3.3.2. To the extent that this process is automated it supposes an advantage with respect to other approaches as [12] and [13], since they started their approaches with a hybrid model without showing how it is achieved. • Mode Reduction: At this point infeasible modes of the hybrid automaton are removed by means of the Z3 solver, in addition, modes describing the same dynamics are removed. The remaining modes are saved and sent to the last step where test coverage is measured. A more in-depth explanation is presented in section 3.3.3. • Triggered modes: The workflow to retrieve the triggered modes during simulation time is shown in Figure 3.5. The input to the algorithm are the conditions of the hybrid DAE and the results of the simulation. The algo- rithm loops through the simulation time and all the conditions are evaluated to check whether they are true or false. As mentioned in section 3.3.2.1, solely one condition in each conditional equation will be evaluated to true. Thus, a mode is identified as the logical conjunction of the conditions evalu- ated to true at each time instant. Following the example of the hybrid DAE in (3.3), at any given time the evaluation of the conditions will give as a solution only one of the modes listed in Table 3.1. When the for loop is completed, the repeated modes are filtered. Likewise, modes with different conditions but representing the same dynamics are also eliminated such that the final output is the minimal set of triggered modes. • Test coverage: At this point, it is now possible to measure test coverage produced by executing a test case on the SUT applying (3.1) which is shown here again for clarity: Mode Coverage = Number of modes exercised during simulation set of reachable modes × 100% (3.2) 21 3. Test Coverage for CPSs • Results.mat • Conditions Hybrid DAE Minimal set of triggered modes i < simulation time? False Evaluate conditions with results.mat file Store triggered modes i = i + 1 Filter repeated modes True Figure 3.5 – Description of the process Triggered modes. The algorithm aims to find the modes triggered during simulation time, starting with the results of the simulation and the conditions retrieved from a hybrid DAE. 3.3.2 Modes: from Hybrid DAE to Hybrid Automaton The procedure developed for constructing hybrid automata relies on the abstrac- tion of hybrid DAEs. To illustrate the steps carried out, a simple example of a hybrid DAE shown in (3.3) is used throughout this section. The example consists of two conditional equations that can take two and three different values (f j i ) de- pending on which of the conditions is true. The conditions, represented as Cj i , are predicate sentences, as for instance “a ≥ 0”, where a can be of type real, integer or boolean. var1 = if C1 1 then f 1 1 elseif C1 2 then f 1 2 (3.3a) var2 =  if C2 1 then f 2 1 elseif C2 2 then f 2 2 elseif C2 3 then f 2 3 (3.3b) 22 3. Test Coverage for CPSs The following simplifications have been made: • In Modelica, conditional equations must have an else statement at the end to cover the case when the rest of conditions are evaluated to false. For clarity purposes, this statement is obviated without loss of generality in the explanation to generate a HA. • Hybrid DAEs can also contain regular equations that are not conditional, though, that sort of equations always exist in all modes so that they can be omitted in the analysis without missing modes. For this simple case, the hybrid DAE in (3.3) results in six modes that are listed in Table 3.1. The hybrid automaton generated is depicted in Figure 3.6 where the automaton consists of 6 modes and 30 transitions. Mode var1 var2 Guard 1 f 1 1 f 2 1 C1 1 ∧ C2 1 2 f 1 1 f 2 2 C1 1 ∧ C2 2 3 f 1 1 f 2 3 C1 1 ∧ C2 3 4 f 1 2 f 2 1 C1 2 ∧ C2 1 5 f 1 2 f 2 2 C1 2 ∧ C2 2 6 f 1 2 f 2 3 C1 2 ∧ C2 3 Table 3.1 – Information that can be extracted from 3.3 to define modes. Each mode has associated a guard as a combination of conditions. Each guard defines the value of the variables var1 and var2 that represents the dynamics of the mode. 3.3.2.1 Identification of modes Hereinafter, the followed procedure identifies modes by its unequivocally associated guard, which is a combination of conditions that must be fulfilled to reach a specific mode. It is easy to see that the maximum number of possible modes can be calculated by multiplying the number of conditions inside each conditional equation with 23 3. Test Coverage for CPSs each other. In the case of 3.3, the number of modes is 2 × 3 = 6. In order to automate the process of mode generation, the set of possible modes is modelled as the cross-product over all the conditions in a hybrid DAE and is represented by the logical formula (3.4). This logical formula is said to be in Conjunctive Normal Form (CNF) and to expand it means to end up doing the cross-product of the elements Ci j. The usefulness of representing modes through a CNF formula will become more clear when explaining the Z3 solver [24] in section 3.3.3.1. Modes = k∧ i=1  ni∨ j=1 Ci j  (3.4) where: k ∈ N = number of conditional equations ni ∈ N = number of conditions at each conditional equation As an example, the result of applying the above formula on the hybrid DAE (3.3) is presented in the below equation (3.5) which spans all the possible modes. Obviously, the modes finally calculated coincide with the modes in table 3.1. Modes = ( C1 1 ∨ C1 2 ) ∧ ( C2 1 ∨ C2 2 ∨ C2 3 ) = (3.5) = ( C1 1 ∧ C2 1 ) ∨ ( C1 1 ∧ C2 2 ) ∨ ( C1 1 ∧ C2 3 ) ∨ ∨ ( C1 2 ∧ C2 1 ) ∨ ( C1 2 ∧ C2 2 ) ∨ ( C1 2 ∧ C2 3 ) A more deep insight into how modes are calculated suggest the following short- comings to be borne in mind when building the hybrid automata: 1) Hybrid automata are able to capture non-deterministic behaviour, i.e., there may also be situations where two or more conditions in a conditional equation are true at the same time. For instance, staying in mode 1, it could happen that conditions C2 1 and C2 2 being true, entailing the possibility that modes 1 and 2 would be active simultaneously, which is physically impossible. In order to achieve deterministic behaviour, the modes should be described in a manner so that two or more conditions can never be true at any given time. In the tool developed along with this work, the procedure followed is illustrated with the guard associated with the mode 1: Mode 1 : 〈( C1 1 ∧ ¬C1 2 ) ∧ ( C2 1 ∧ ¬ ( C2 2 ∨ C2 3 ))〉 The above mode can solely be reached when C1 1 and C2 1 are true and C1 2 , C2 2 and C2 3 false. 24 3. Test Coverage for CPSs 2) Not all guards are feasible; it can occur that some conditions in a guard contradict each other. For instance, the mode 1 with guard 〈C1 1 ∧ C2 1〉 where C1 1 = current < 0 and C2 1 = current ≥ 0 will be always false, meaning that this mode does not exist. The SMT Z3 tool is used in order to identify such contradictions and remove the infeasible modes generated by (3.4). This process significantly reduces the number of modes in the system. 3) Several conditions Cj i in (3.3) may update a variable to the same value so that different guards would define the same mode. Looking at table 3.1, it could happen that f 2 1 = f 2 3 so that mode 1 = mode 3 and mode 4 = mode 6, thus, the created automaton has four modes instead of 6. This possibility is exploited to further decrease the number of modes in the HA. 25 3. Test C overage for C PSs Mode 1 𝐶1 1 ∧ 𝐶1 2 Mode 2 𝐶1 1 ∧ 𝐶2 2 Mode 3 𝐶1 1 ∧ 𝐶3 2 Mode 4 𝐶2 1 ∧ 𝐶1 2 Mode 5 𝐶2 1 ∧ 𝐶2 2 Mode 6 𝐶2 1 ∧ 𝐶3 2 𝐶1 2 𝐶2 2 𝐶2 2 𝐶3 2 𝐶1 2 𝐶2 2 𝐶2 2 𝐶3 2 𝐶1 2 𝐶3 2 𝐶1 2 𝐶3 2 Mode 4 Mode 1 Mode 6 Mode 3 𝐶1 1𝐶2 1𝐶1 1𝐶2 1 𝐶1 1𝐶2 1 𝐶1 1 ∧ 𝐶1 2 𝐶1 1 ∧ 𝐶2 2 𝐶2 1 ∧ 𝐶1 2 𝐶2 1 ∧ 𝐶2 2 𝐶1 1 ∧ 𝐶2 2 𝐶1 1 ∧ 𝐶3 2 𝐶2 1 ∧ 𝐶2 2 𝐶2 1 ∧ 𝐶3 2 𝐶1 1 ∧ 𝐶3 2 𝐶2 1 ∧ 𝐶1 2 𝐶1 1 ∧ 𝐶1 2 𝐶2 1 ∧ 𝐶3 2 Figure 3.6 – Hybrid automaton abstracted from the hybrid DAE in 3.3. 26 3. Test Coverage for CPSs 3.3.3 Mode Reduction The mode reduction step is based on the use of the Satisfiability Modulo Theories, there- fore, first is introduced the Z3 solver and later is presented the workflow to reduce the number of modes. 3.3.3.1 Satisfiability Modulo Theories - the Z3 Solver The Z3 solver is a Satisfiability Modulo Theories (SMT) solver developed by L. de Moura and N. Bjørner at Microsoft Research [24]. An SMT solver is such that given a logical formula in first-order logic, it decides whether it is satisfiable or not. A formula F is said to be satisfiable when exists a valuation that makes F true. In the SMT context, the input to the solver represents a constraint system that the solver will try to satisfy providing a solution. In order to illustrate the operation of the solver is presented an example in Figure 3.7, that uses two different formulas. The first case is decided to be satisfiable and a solution is provided while for the second case no solution is returned since the formula is unsatisfiable. x = Int('x') y = Int('y') solve( And ( x > 5, y<7, y == x+5)) ------------------------------------------ check(): unsat Solution : no solution x = Int('x') y = Int('y') solve( And ( x > 5, y == x+5)) ------------------------------------------ check(): sat Solution: [x = 6, y = 11] a) sat b) unsat Figure 3.7 – Example of how the Z3 solver checks satisfiability. First are defined the variables x and y, then a constraint is added to the solver. With the check command the solver decides whether the formula has a solution or not, if yes a solution is displayed. The logical formulas used in the fore-mentioned example are the same sort of formula as was used in (3.5) to identify all modes: both are logical formulas that uses predicates. Obviously, this was not a coincidence but a deliberate choice in favor of using the Z3 solver to analyse modes. Primarily, the objective is to check satisfiability for all modes in order to remove those that are false. Among different SMT solvers, Z3 was selected because of the following reasons: • It is free available for academic purposes. Licensed with Microsoft Research License Agreement (MSR-LA). • It has interfaces API’s in several languages, in particular, in Python which is the language used to develop test coverage in this thesis. • If a formula is satisfiable, SMT Z3 returns a solution which is an useful property used during the development of the algorithm to perform test coverage. • It is a high-performance theorem prover. In the SMT Competition at 2014 SMT Z3 participated as a reference for the other competitors. 27 3. Test Coverage for CPSs For the time being, the Z3 solver supports nonlinear polynomial Real arithmetic but cannot handle transcendental functions such as sine, cosine and exponential. [25]. 3.3.3.2 Mode Reduction Workflow The number of modes increases as the level of complexity of the DAEs raise. As com- mented in the earlier section 3.3.2.1, the combination of conditions easily leads to infeasible modes that can be removed applying the Z3 tool. More accurately, the Z3 solver selects the feasible modes among all possible modes. Figure 3.8 shows the algorithm to perform reduction of modes, which is divided into two main parts: firstly, all possible modes are sent to the Z3 solver as an input, through (3.4). The core of the method is a while loop checking whether the set of added constraints is satisfiable or unsatisfiable. If satisfiable, Z3 returns a solution that is mathematically coherent and represents a feasible mode in the model. Later, the mode is negated and forwarded to the solver as a new constraint, such that at the next time the solver is checking satisfiability it will not return the same solution. When the model is decided to be unsatisfiable the search of feasible modes is completed. In the second part of the algorithm, further reduction of modes is achieved by removing those describing same dynamics to obtain the minimal set of modes in the system. Check SAT ? sat unsat Add to Solver Constraint: ¬ Mode Mode Stored feasible Modes Filter repeated Modes Solution Minimal set of feasible modes i=1 k j=1 ni Gj i Figure 3.8 – Mode reduction algorithm. A set of constraints representing modes of a HA is added to the solver through a logical formula. The solver checks satisfiability and if satisfiable it returns a solution that is negated and added back to the solver. This loop is repeated until the constraints are unsatisfiable, thus, concluding the process. Finally, modes describing identical behaviours are removed. A simple example describing the operation of the Z3 solver to identify satisfiable modes is presented in Figure 3.9. The input to the algorithm is the constraint (x < 0∨ y < 0)∧ 28 3. Test Coverage for CPSs (x ≥ 0∨y ≥ 0) that has only two satisfiable solutions: 〈x < 0 ∧ y ≥ 0〉 or 〈y < 0 ∧ x ≥ 0〉. The first time that satisfiability is checked (line 17), the solver returns a solution that is added back to the solver as a constraint using the logical Not. The second time the solver tries to solve the constraints, it returns the other solution that is also added to the solver as a constraint. When the solver inspect the constraints to find a solution for the third consecutive time, it is decided to be unsatisfiable as expected. 1 >> x , y = Int ( ' x y ' ) // Dec la ra t i on o f i n t e g e r v a r i a b l e s 2 >> p1 , p2 , p3 , p4 = Bools ( ' p1 p2 p3 p4 ' ) // Dec la ra t i on o f boolean v a r i a b l e s 3 4 >> s l v = So lve r ( ) // c r e a t i n g the o b j e c t s o l v e r 5 >> s l v . add (And(Or(x<0,y<0) ,Or(x>=0,y>=0))) // adding the input to the s o l v e r 6 7 // boo leans f o r keeping t rack the d i f f e r e n t c o n d i t i o n s p r e v i o u s l y added 8 >> s l v . add ( p1 == (x<0) , p2 == (y<0) , p3 == (x>=0), p4 == (y>=0)) 9 10 >> s l v . a s s e r t i o n s ( ) // Shows cur rent c o n s t r a i n t s in the So lve r 11 [ And(Or( x < 0 , y < 0) , Or( x >= 0 , y >= 0 ) ) , 12 p1 == ( x < 0) , 13 p2 == ( y < 0) , 14 p3 == ( x >= 0) , 15 p4 == ( y >= 0 ) ] 16 17 >> s l v . check ( ) // check ing s a t i s f i a b i l i t y 18 sa t // returned value . Const ra in t s are S a t i s f i a b l e 19 20 >> s l v . model ( ) // s o l v i n g the c o n s t r a i n t s 21 [ x = −1, // returned s o l u t i o n 22 y = 0 , 23 p1 = True , // f e a s i b l e mode = 〈p1 ∧ p4〉 = 〈x < 0 ∧ y ≥ 0〉 24 p2 = False , 25 p3 = False , 26 p4 = True ] 27 28 // adding the f e a s i b l e mode as a c o n s t r a i n t to the s o l v e r 29 >> s l v . add ( Not (And( p1 , p4 ) ) ) 30 31 >> s l v . check ( ) // check ing s a t i s f i a b i l i t y 32 sa t // s a t i s f i a b l e c o n s t r a i n t s 33 34 >> s l v . model ( ) // s o l v i n g the c o n s t r a i n t s 35 [ x = 0 , // s o l u t i o n 36 y = −1, 37 p1 = False , // f e a s i b l e mode = 〈p2 ∧ p3〉 = 〈y < 0 ∧ x ≥ 0〉 38 p2 = True , 39 p3 = True , 40 p4 = False ] 41 42 // adding the f e a s i b l e mode as a c o n s t r a i n t to the s o l v e r 43 >> s l v . add ( Not (And( p2 , p3 ) ) ) 44 45 >> s l v . check ( ) // check ing s a t i s f i a b i l i t y 46 unsat // U n s a t i s f i a b l e Figure 3.9 – Description of the operation of the Z3 solver in the mode reduction algo- rithm. Starting with the formula (x < 0∨ y < 0)∧ (x ≥ 0∨ y ≥ 0), the Z3 solver returns all the possible solutions until the constraints are unsatisfiable. Lines started with “>>” are commands written in the Python console, the rest of lines are the solutions provided by the Z3 solver. The script was coded using the Z3 API in Python 29 4 Case study, Dog-Clutch This chapter focuses on the results of applying the algorithm described in section 3.3.1 to measure test coverage for the case study, the Dog-clutch model provided by Volvo Cars Corporation. The system proposed is simple but complicated enough to carry on the objectives stated in the beginning of this master thesis. The first part of the section is dedicated to describe the dog-clutch system and the second part evaluates the results obtained. 4.1 Description of the Dog-Clutch A dog-clutch is a mechatronic system. The following elements characterize its mechatronic nature: a) Mechanical system: The physical system is composed by the following mechanical components: Dog-clutch, Cam-Ring and Spring. This is the plant of the model that determines the dynamical properties of the system. b) Computer Device: All the information from the communication devices is gath- ered, processed and forwarded to the actuators by an electronic control unit. This implements a closed loop control algorithm that determines the logical attributes of the system. c) Communications: The communication between the computer device and the physical system is done by means of a solenoid playing the role of an actuator and positioning sensors providing feedback to the control algorithm. EM Dog- clutch shaft 1 shaft 2 Figure 4.1 – Initially, the electric motor transmits the torque generated to the shaft 1. Then, the function of the dog-clutch is to propagate the torque in the shaft 1 to the shaft 2 that is connected to the wheels. 30 4. Case study, Dog-Clutch a) b) c) d) Figure 4.2 – Example of a dog-clutch system. a) Image of a real dog-clutch. b) dis- engaged state, the cam-ring is static c) synchronizing phase, the cam-ring starts moving in the same direction as the Dog-Clutch. A control algorithm synchronizes the velocity of the two parts to achieve the optimal position to engage. d) engagement phase, both components rotate with the same velocity. Cam-Ring begins to move axially until both parts are engaged. Figure provided by Volvo Car Corporation. The function of a dog-clutch is to engage two rotating shafts to propagate motion. In the case studied here, the torque generated by an electric motor is transmitted to the wheels in order to move the vehicle as shown in Figure 4.1. The operation of the clutch system is shown in Figure 4.2, where the three main states are described. It consists of two pieces, a dog-clutch and a cam-ring that meshes together by moving the cam-ring towards the dog-clutch. The movement of the cam-ring is produced by an anchor that pushes it when a solenoid is energised. To disengage the system the solenoid must be deactivated. When the velocity of the two parts is synchronised the cam-ring moves axially to engage with the clutch-dog. This axial displacement is done through a solenoid controlled by current. 4.1.1 Modelling the Dog-Clutch The starting point was the clutch model provided by Volvo Car Corporation, which was implemented in Simscape™. Though, since OpenModelica was the chosen tool for simula- tion purposes, the model was translated from Simscapre to Modelica language. Since both environments share the acausal modelling approach1, it facilitated the code translation task. The final version of the code is presented in Appendix A. It must be mentioned how the acausal approach influences the style of coding. Firstly, for all variables and parameters, it must be indicated the type (real, integer, boolean, ...). Secondly, all the variables must have assigned a physical quantity so that units are consistent in the equations. Finally, there is a specific section called equation where, as the name suggests, equations describing the system are added. Recall that equations are not assignments but relations between physical quantities. The equation section is declared using an if-then-else structure that imposes the logics of the system, i.e. it represents the discrete dynamics of the system. Each conditional statement (if, elseif, else) is used to define a new situation where a set of equations describes the continuous behaviour at that state. In total, 20 distinct scenarios of the system are modelled and have been commented inside the Modelica code. The following variables and parameters forms the conditions statements defining the fore-mentioned scenarios: 1The characteristics of this approach are described in more detail in section 2.2.1 31 4. Case study, Dog-Clutch • z (m): Is a variable of the model used to describe the distance between the dog- clutch and the cam-ring as it can be seen in Figure 4.3. • ω (rad/s): Is an input of the model describing the angular velocity difference between the dog-clutch and the cam-ring • a (rad): Is a variable of the model describing the backlash phenomenon. • Z0, Z1 (m): Are internal parameters of the model describing distance limits, shown in Figure 4.3. • alim (m): Defines a half of backlash. Is a parameter of the model. • wlim (rad/s): Specifies the maximum value of ω to engage the system. Is a parameter of the model. • engage_req: Defines with a 1 or 0 whether engage of the clutch is required. Is a parameter of the model. • prev_eng_state: Binary number that informs about the state of the clutch in the previous time instant. Is a parameter of the model. 𝑍0𝑍1 𝑍 = 0 Figure 4.3 – The variable Z defines the distance between the two parts of the system. Z0 delimits when the dog-clutch reaches the cam-ring. Z1 delimits when the dog-clutch reaches the final position. The importance of these variables and parameters lies in the fact that they will form the guards enabling transitions in the hybrid automaton used to analyse test coverage. 32 4. Case study, Dog-Clutch 4.2 Implementation and evaluation The Python programming language was used to implement the tool that performs test coverage. It was chosen primarily because of two reasons: (1) it is an efficient language manipulating strings so it is adequate to parse Hybrid DAEs provided by OpenModelica; (2) the Z3 solver has an API in Python so that it is easier to use it. The implementation of the proposed algorithm is presented following the chain of processes described in Figure 3.4 and will help to discuss the shortcomings encountered. • Inputs: A model of the Dog-Clutch implemented in Modelica language and a test case in form of CSV file were the inputs of the algorithm. The first can be seen in the Appendix A and the test case was chosen randomly with the only requirement that the values of the variables should be inside the physical margins of the model. • OpenModelica: The main Python application launched the OpenModelica soft- ware and created the hybrid DAE structure shown in Appendix B and a Matlab file with the results of the simulation. In the hybrid DAE two type of equations can be distinguished, one one hand, there are five simple assignment equations as those in lines 2, 3, 4, 5 and 6, in the other hand, four conditional equations in lines 1, 7, 21 and 30 that will be used to generate the modes of the HA. The conditions in these equations are expressions made up from the variables described in section 4.1.1. • Modes: To identify all the possible modes contained in the original model, the conditions in each conditional equation were parsed in two different formats: Python and Z3. The reason for this was that the Z3 solver requires inputs in a specific format while the Python format was used to evaluate whether the conditions were true or false. A future work could be to improve the algorithm so that Z3 format can be used in both cases simplifying the parsing step. Finally, 48 conditions were obtained distributed as follows: Conditional equation Nr. of conditions Engage_req 2 DER.zv 20 t 12 eng_state 14 Table 4.1 – Number of conditions for each conditional equation described in the hybrid DAE structure shown in Appendix B. As example, the conditions obtained after parsing the equation t are shown in Table 4.2. The total number of modes obtained at this stage is the cross product of the con- ditions found, for the case study: {2} × {20} × {12} × {14} = 6720. This number includes the infeasible modes that should be removed. • Mode Reduction: After running the Z3 solver on python, only 34 of the 6720 modes were decided to be logical, which clearly represents a huge reduction in the amount of modes. The execution time of only 0.6 seconds performed by the Z3 solver was another pleasant surprise. Definitely, these two facts evidence the effectiveness reached by the solver. Further reduction of modes was achieved by checking the 33 4. Case study, Dog-Clutch dynamics described by those modes, resulting in 20 different behaviours that are shown in Table 4.3 where for each mode is shown the value assigned to each variable. Some problem were found when examining the results: a) Mode 1 is unreachable and it appears due to the way the Modelica causal approach describes models. b) 10 modes out of the 20 modes do not exist in the original model. These two points falsifies the measure of test coverage since 100% will never be reached, this is a task to solve in future work. • Triggered Modes: For the test case created, only nine modes were exercised throughout the simulation, they are identified in Table 4.3 with an asterisk. This is the more time consuming step of the proposed methodology since 48 conditions are evaluated at each time instant. • Test coverage: The result of measuring test coverage is displayed and dumped into a txt file as in Figure 4.4. For the case study and using the inputs described above, only 45% of the feasible modes were exercised, indicating, that more test cases are needed to achieve higher coverage. Besides the numerical results, more information about the model can be dumped into the txt file as the triggered and feasible modes including the conditions that composes them. The results obtained here are considered useful for two reasons: a) the identified modes no triggered by the test case can be used as clues in an algorithm to automatically generate new test cases that increase the test coverage measure. The automated generation of test cases is the final objective of the model-based testing methods. b) numerically quantify how well a mechatronic system is tested. It must be noted that the final methodology implemented in this thesis generates modes that are not reachable so that 100% coverage could be impossible to reach as it happens with the case study analysed in this work. 1 Mode Coverage : 45.00% 2 3 F e a s i b l e Modes : 20 V i s i t e d Modes : 9 Figure 4.4 – Result of measuring test coverage using mode coverage as a criterion. Feasible modes are those that are mathematically coherent while visited modes are modes that have been exercised by a specific test case during simulation. 34 4. C ase study,D og-C lutch t_C0 = (engage_req == 1 and prev_eng_state == 0) and (z < 0.0016) and (not ((z >= 0.0016 and abs(w) > w_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) <= a_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) > a_lim))) t_C1 = (engage_req == 1 and prev_eng_state == 0) and (z >= 0.0016 and abs(w) > w_lim) and (not ((z < 0.0016) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) <=a_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) >a_lim))) t_C2 = (engage_req == 1 and prev_eng_state == 0) and (z >= 0.0016 and abs(w) <= w_lim and abs(a) <=a_lim) and (not ((z < 0.0016) or (z >= 0.0016 and abs(w) > w_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) >a_lim))) t_C3 = (engage_req == 1 and prev_eng_state == 0) and (z >= 0.0016 and abs(w) <= w_lim and abs(a) >a_lim) and (not ((z < 0.0016) or (z >= 0.0016 and abs(w) > w_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) <=a_lim))) t_C4 = (engage_req == 1 and prev_eng_state == 0) and (not ((z < 0.0016) or (z >= 0.0016 and abs(w) > w_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) <=a_lim) or (z >= 0.0016 and abs(w) <= w_lim and abs(a) >a_lim))) t_C5 = (engage_req == 1 and prev_eng_state == 1) and (abs(a) >a_lim and z < 0.0032 and z >= 0.0016) and (not ((abs(a) >a_lim and z >= 0.0032 and z >= 0.0016))) t_C6 = (engage_req == 1 and prev_eng_state == 1) and (abs(a) >a_lim and z >= 0.0032 and z >= 0.0016) and (not ((abs(a) >a_lim and z < 0.0032 and z >= 0.0016))) t_C7 = (engage_req == 1 and prev_eng_state == 1) and (not ((abs(a) >a_lim and z < 0.0032 and z >= 0.0016) or (abs(a) >a_lim and z >= 0.0032 and z >= 0.0016))) t_C8 = (engage_req == 0 and prev_eng_state == 1) and (abs(a) >a_lim and z >= 0.0016) and (not ()) t_C9 = (engage_req == 0 and prev_eng_state == 1) and (not ((abs(a) >a_lim and z >= 0.0016))) t_C10 = (engage_req == 0 and prev_eng_state == 0) t_C11 = not ((engage_req == 1 and prev_eng_state == 0) or (engage_req == 1 and prev_eng_state == 1) or (engage_req == 0 and prev_eng_state == 1) or (engage_req == 0 and prev_eng_state == 0)) Table 4.2 – Conditions extracted from the conditional equation t after parsing the Hybrid DAE in Appendix B. In this case the conditions were parsed to Python format 35 4. C ase study,D og-C lutch engage_req engage_state t mass · der(zv) Mode 1 0 0 0 0 Mode 2 0 0 0 f_spring −DampingBelleville_extra · zv Mode 3 * 0 1 W BD · w + stiff · (−0.00437 + abs(a)) · (·Real·)(sign(a)) f_spring −W SD · (−0.0016 + z) · zv Mode 4 0 0 HiSpeedDamping2 · w f_spring − stiff2 · (−0.0016 + z) Mode 5 0 0 LoSpeedDamping2 · w f_spring − stiff2 · (−0.0016 + z) Mode 6 0 1 W BD · w + stiff · (−0.00437 + abs(a)) · (·Real·)(sign(a)) f_spring − stiff2 · (−0.0032 + z)−W SD · (−0.0016 + z) · zv Mode 7 0 0 0 f_spring − stiff2 · (−0.0016 + z) Mode 8 0 1 0 f_spring − stiff2 · (−0.0032 + z) Mode 9 * 0 0 0 f_spring Mode 10 * 0 1 0 f_spring Mode 11 1 0 0 0 Mode 12 1 0 0 f_spring −DampingBelleville_extra · zv Mode 13 * 1 1 W BD · w + stiff · (−0.00437 + abs(a)) · (·Real·)(sign(a)) f_spring −W SD · (−0.0016 + z) · zv Mode 14 1 0 HiSpeedDamping2 · w f_spring − stiff2 · (−0.0016 + z) Mode 15 * 1 0 LoSpeedDamping2 · w f_spring − stiff2 · (−0.0016 + z) Mode 16 * 1 1 W BD · w + stiff · (−0.00437 + abs(a)) · (·Real·)(sign(a)) f_spring − stiff2 · (−0.0032 + z)−W SD · (−0.0016 + z) · zv Mode 17 1 0 0 f_spring − stiff2 · (−0.0016 + z) Mode 18 * 1 1 0 f_spring − stiff2 · (−0.0032 + z) Mode 19 * 1 0 0 f_spring Mode 20 * 1 1 0 f_spring Table 4.3 – Feasible Modes obtained by the developed application. Each mode is defined by four variables that change its dynamic at different modes. The asterisk indicates the modes exercised by the specific test case used during simulation. 36 5 Conclusion A new approach to measure test coverage for systems with continuous dynamics is pre- sented. The developed algorithm supports the use of Modelica language to describe CPSs in form of hybrid automata which can be used to define test coverage. Mode coverage has been identified to be a good candidate as coverage criterion since it is able to capture the infiniteness of the continuous dynamics of the CPSs in a finite set of modes, which allow implementing quantitative methods to measure test coverage. The study carried out in this thesis has examined the procedure to abstract CPSs implemented by means of an acausal approach into a mathematical description of a hy- brid automaton. The results are promising to the extent that Hybrid DAEs created by OpenModelica can be used to automate the process of mode generation and measuring coverage. The results given by the algorithm permit to discover untested areas in the system and provide clues to guide the generation of new test cases to cover such areas, which is the main objective of Model-Based Testing approach. The approach followed can also enhance other testing methods in order to support testing of hybrid systems. With regard to the reduction mode technique implemented, it is worth to remark the high performance shown by the Z3 solver to decide satisfiability and to remove infeasible modes yielding more accurate results. The approach proposed here could not have been achieved unless the enormous progress and development conducted in SMT solvers in recent times. The usefulness of this approach still requires more development and testing with more general CPSs models in order to guarantee that software as OpenModelica always pro- duces hybrid DAEs that are suitable to be transformed into hybrid automata. In addition, the Z3 solver also should be assessed against more complex models to verify its perfor- mance. 5.1 Limitations This work succeeded in proving the validity of the methodology proposed, though, some limitations have been found, further described below. a) The algorithm has been tested in a single, simple but still complex example to be able to assess the developed application. b) The Z3 solver does not check for reachability, therefore it may happen that the algorithm generates feasible modes that are unreachable or physically impossible. c) Z3 do not support real transcendental functions, e.g. sine, cosine and exponential. Thus, transcendental functions are not allowed in the conditions. 37 5. Conclusion 5.2 Future Work This section presents the future work that can be done based on the results presented in this master’s thesis. • Generate test cases: The next natural step would be to develop a tool that automates the process to generate test cases to explore the localised untested areas, i.e. to continue with the implementation of the model-based testing methodology. • Verification against more complex systems: The developed application has been tested only against one mechatronic system so more cases are necessary to verify the generation of hybrid automata and more thoroughly evaluate the approach followed. • Improve Reduction of modes: In order to achieve an accurate test coverage measure, it is necessary to refine the mode reduction process to remove non-existent modes in the hybrid automata. • Analyse HA under other criteria: Besides mode coverage criterion, other criteria such as transition coverage can be carried out to guarantee correctness. In addition, it would be interesting to analyse how well the continuous dynamic is tested within each mode. 38 Bibliography [1] S. Miremadi, Modellbaserad testning av mekatroniska system (testron) - vinnova, 2016. [Online]. Available: http : / / www . vinnova . se / sv / Resultat / Projekt / Effekta/2009- 02186/Modellbaserad- Testning- av- Mekatroniska- System- TESTRON/ (visited on 09/02/2016). [2] R. Alur, Principles of cyber-physical systems. MIT Press, 2015. [3] E. A. Lee, “Cyber physical systems: Design challenges”, in 2008 11th IEEE In- ternational Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), IEEE, 2008, pp. 363–369. [4] M. Utting, A. Pretschner, and B. Legeard, “A taxonomy of model-based testing approaches”, Software Testing, Verification and Reliability, vol. 22, no. 5, pp. 297– 312, 2012. [5] M. Conrad, “Verification and validation according to iso 26262: A workflow to fa- cilitate the development of high-integrity software”, Embedded Real Time Software and Systems (ERTS2 2012), 2012. [6] M. A. Mäkinen, “Model based approach to software testing”, PhD thesis, Citeseer, 2007. [7] D. Firesmith, Four types of shift left testing, 2017. [Online]. Available: https:// insights.sei.cmu.edu/sei_blog/2015/03/four- types- of- shift- left- testing.html (visited on 01/06/2017). [8] J. Eddeland, J. Gil, R. Fransen, S. Miremadi, M. Fabian, and K. Åkesson, Automated mode coverage analysis for model-based testing of hybrid automata, 2016. [9] R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho, “Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems”, in Hybrid systems, Springer Berlin Heidelberg, 1993, pp. 209–229. [10] J.-F. Raskin, “An introduction to hybrid automata”, in Handbook of networked and embedded control systems, Springer, 2005, pp. 491–517. [11] T. A. Henzinger, “The theory of hybrid automata”, in Verification of Digital and Hybrid Systems, Springer, 2000, pp. 265–292. [12] A. A. Julius, G. E. Fainekos, M. Anand, I. Lee, and G. J. Pappas, “Robust test generation and coverage for hybrid systems”, in International Workshop on Hybrid Systems: Computation and Control, Springer, 2007, pp. 329–342. [13] T. Nahhal and T. Dang, “Test coverage for continuous and hybrid systems”, in International Conference on Computer Aided Verification, Springer, 2007, pp. 449– 462. [14] J. Kapinski, J. Deshmukh, X. Jin, H. Ito, and K. Butts, “Simulation-guided ap- proaches for verification of automotive powertrain control systems”, in 2015 Amer- ican Control Conference (ACC), IEEE, 2015, pp. 4086–4095. 39 http://www.vinnova.se/sv/Resultat/Projekt/Effekta/2009-02186/Modellbaserad-Testning-av-Mekatroniska-System-TESTRON/ http://www.vinnova.se/sv/Resultat/Projekt/Effekta/2009-02186/Modellbaserad-Testning-av-Mekatroniska-System-TESTRON/ http://www.vinnova.se/sv/Resultat/Projekt/Effekta/2009-02186/Modellbaserad-Testning-av-Mekatroniska-System-TESTRON/ https://insights.sei.cmu.edu/sei_blog/2015/03/four-types-of-shift-left-testing.html https://insights.sei.cmu.edu/sei_blog/2015/03/four-types-of-shift-left-testing.html https://insights.sei.cmu.edu/sei_blog/2015/03/four-types-of-shift-left-testing.html Bibliography [15] R. Agrawal, “Semi-automated formalization and verification of automotive require- ments using simulink design verifier”, 2015. [16] 2016. [Online]. Available: https : / / se . mathworks . com / products / simulink/ (visited on 11/30/2016). [17] 2016. [Online]. Available: https : / / se . mathworks . com / products / simscape/ (visited on 11/30/2016). [18] 2016. [Online]. Available: https://www.openmodelica.org/ (visited on 11/30/2016). [19] P. Fritzson and et. al., Openmodelica system documentation, 2014-02-01 for Open- Modelica 1.9.1 Beta1. Open Source Modelica Consortium, 2014, p. 14. [Online]. Available: https://openmodelica.org/svn/OpenModelica/trunk/doc/OpenMode licaUsersGuide.pdf (visited on 09/12/2016). [20] A. Baresel, M. Conrad, S. Sadeghipour, and J. Wegener, “The interplay between model coverage and code coverage”, in Proc. EuroCAST, 2003, pp. 136–190. [21] G. J. Myers, C. Sandler, T. Badgett, and T. M. Thomas, “The art of software testing .”, 2004. [22] 2016. [Online]. Available: https://gcc.gnu.org/onlinedocs/gcc/Gcov.html (visited on 12/10/2016). [23] 2017. [Online]. Available: http://releases.llvm.org/download.html. [24] L. De Moura and N. Bjørner, “Z3: An efficient smt solver”, in International con- ference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, pp. 337–340. [25] L. De Moura, Z3 supports for nonlinear arithmetics, 2016. [Online]. Available: http: //stackoverflow.com/questions/18064822/z3- supports- for- nonlinear- arithmetics (visited on 12/21/2016). 40 https://se.mathworks.com/products/simulink/ https://se.mathworks.com/products/simscape/ https://www.openmodelica.org/ https://openmodelica.org/svn/OpenModelica/trunk/doc/OpenModelicaUsersGuide.pdf https://openmodelica.org/svn/OpenModelica/trunk/doc/OpenModelicaUsersGuide.pdf https://gcc.gnu.org/onlinedocs/gcc/Gcov.html http://releases.llvm.org/download.html http://stackoverflow.com/questions/18064822/z3-supports-for-nonlinear-arithmetics http://stackoverflow.com/questions/18064822/z3-supports-for-nonlinear-arithmetics http://stackoverflow.com/questions/18064822/z3-supports-for-nonlinear-arithmetics A Clutch Model [] Listing A.1 – Clutch model implemented in Modelica language 1 encapsulated model c l u t c h 2 import Mode l i ca .Cons tant s .p i ; 3 import M o d e l i c a . S I u n i t s . {Torque , Current , Ve loc i ty , Mass , Trans lat iona lSpr ingConstant , 4 RotationalDampingConstant , TranslationalDampingConstant , Angle , Length , 5 Rotat ionalSpr ingConstant , AngularVeloc ity , E l ec t r i ca lForceCons tant , 6 DynamicViscosity , Frequency } ; 7 8 // PARAMETERS 9 parameter Frequency freqHz = 1 ; 10 parameter Mass mass = 0 .15 ; 11 parameter Trans la t iona lSpr ingConstant k_spring = 100 ; 12 parameter RotationalDampingConstant WallBounceDamping = 10 ; 13 parameter TranslationalDampingConstant DampingBe l l ev i l l e = 10 ; 14 parameter DynamicViscosity WallScrapeDamp = 1 e3 ; 15 parameter TranslationalDampingConstant DampingBel l ev i l l e_extra = 100 ; 16 parameter Angle ph i_ in i t = 0 ; 17 parameter Length z_in i t = 0 ; 18 parameter Rotat iona lSpr ingConstant s t i f f = 1 e4 ; 19 parameter Trans la t iona lSpr ingConstant s t i f f 2 = 1 e5 ; 20 parameter RotationalDampingConstant HiSpeedDamping2 = 0 .01 ; 21 parameter RotationalDampingConstant LoSpeedDamping2 = 0 .01 ; 22 parameter E l e c t r i c a l F o r c e C o n s t a n t KI = k_spring ∗ z1 / Iho ld ; 23 24 25 // VARIABLES 26 I n t e g e r eng_state ( s t a r t = 0 , f i x e d = true ) ; 27 I n t e g e r engage_req ; 28 I n t e g e r prev_eng_state ; 29 Real a ; // Backlash ang le ( rad ians ) 30 Real f_spring_n_current ; // Force e x e r c i s e d by the sp r i ng 31 Torque t ( s t a r t = 0 ) ; // due to F r i c t i o n 32 Length z ( s t a r t = z_init , f i x e d = true ) ; // p o s i t i o n 33 Ve lo c i ty zv ( s t a r t = 0 , f i x e d = true ) ; // v e l o c i t y 34 Angle phi ( s t a r t = phi_in it , f i x e d = true ) ; // r o t a t i o n a l ang le 35 36 // INPUTS FROM AN EXTERN FILE 37 input Current cur rent ; 38 input AngularVeloc i ty w; 39 40 // PROTECTED VARIABLES 41 protected 42 constant Real a_lim = s i n ( d e l t a / 2 ) ; 43 constant Real wmax = 3 ; 44 constant I n t e g e r p = 36 ; 45 constant AngularVeloc i ty w_lim = 30 ∗ ( p i / 3 0 ) ; // Speed t r e s h o l d f o r engaging the c l u t c h 46 constant Angle d e l t a = 0 . 5 ∗ ( p i / 1 8 0 ) ; 47 constant Length z0 = 1 .6e −3; // d i s t a n c e to s t a t o r t ee th 48 constant Length z1 = 3 .2e −3; // d i s t a n c e to f u l l y engaged 49 constant Current I c l = 2 . 3 ; 50 constant Current Iho ld = 1 . 2 ; 51 constant Current current_min = 0 .01 ; 52 constant Length dog2dog_range = 0 .2e −3; I A. Clutch Model 53 54 // EQUATION SECTION 55 equation 56 prev_eng_state = pre ( eng_state ) ; 57 w = der ( phi ) ; 58 zv = der ( z ) ; 59 a = s i n (p ∗ phi ) / p ; 60 f_spring_n_current = KI ∗ cur rent − k_spring ∗ z − DampingBe l l ev i l l e ∗ zv ; 61 i f cur rent > current_min then 62 engage_req = 1 ; 63 else 64 engage_req = 0 ; 65 end i f ; 66 i f engage_req == 1 and prev_eng_state == 0 then 67 // engage requested , c l u t c h out o f the cam−r i n g 68 i f z < z0 then 69 // Rotor has not reached s t a t o r 70 eng_state = 0 ; 71 t = 0 ; 72 mass ∗ der ( zv ) = f_spring_n_current ; 73 e l s e i f z >= z0 and abs (w) > w_lim then 74 // Rotor has reached s t a t o r 75 // Speed d i f e f r e n c e too la rge , g l i d e on tee th 76 eng_state = 0 ; 77 t = HiSpeedDamping2 ∗ w; 78 mass ∗ der ( zv ) = f_spring_n_current − s t i f f 2 ∗ ( z − z0 ) ; 79 e l s e i f z >= z0 and abs (w) < w_lim and abs ( a ) <= a_lim then 80 // Rotor has reached s t a t o r 81 // Speed d i f f e r e n c e OK 82 // Tooth with in gap bounds , engage c l u t c h and move forward 83 eng_state = 1 ; 84 t = 0 ; 85 mass ∗ der ( zv ) = f_spring_n_current ; 86 e l s e i f z >= z0 and abs (w) < w_lim and abs ( a ) > a_lim then 87 // Rotor has reached s t a t o r 88 // Speed d i f f e r e n c e OK 89 // Tooth o u t s i d e gap bounds 90 eng_state = 0 ; 91 t = LoSpeedDamping2 ∗ w; 92 mass ∗ der ( zv ) = f_spring_n_current − s t i f f 2 ∗ ( z − z0 ) ; 93 else 94 eng_state = 0 ; 95 t = 0 ; 96 mass ∗ der ( zv ) = 0 ; 97 end i f ; 98 e l s e i f engage_req == 1 and prev_eng_state == 1 then 99 // engage requested , Clutch engaged in prev ious s t a t e 100 i f abs ( a ) > a_lim and z < z1 and z >= z0 then 101 // tee th in the gap , h i t t i n g the wa l l bounds , c l u t c h not in f i n a l p o s i t i o n 102 eng_state = 1 ; 103 t = s t i f f ∗ ( abs ( a ) − a_lim ) ∗ s i g n ( a ) + WallBounceDamping ∗ w; 104 mass ∗ der ( zv ) = f_spring_n_current − WallScrapeDamp ∗ ( z − z0 ) ∗ zv ; 105 e l s e i f abs ( a ) > a_lim and z >= z1 and z >= z0 then 106 // tee th in the gap , h i t t i n g the wa l l bounds , c l u t c h not in f i n a l p o s i t i o n 107 eng_state = 1 ; 108 t = s t i f f ∗ ( abs ( a ) − a_lim ) ∗ s i g n ( a ) + WallBounceDamping ∗ w; 109 mass ∗ der ( zv ) = f_spring_n_current − s t i f f 2 ∗ ( z − z1 ) − WallScrapeDamp∗ 110 ∗ ( z − z0 ) ∗ zv ; 111 e l s e i f abs ( a ) <= a_lim and z < z1 and z >= z0 then 112 // tee th in the gap , not h i t t i n g the wa l l bounds , c l u t c h not in f i n a l p o s i t i o n 113 eng_state = 1 ; 114 t = 0 ; 115 mass ∗ der ( zv ) = f_spring_n_current ; 116 e l s e i f abs ( a ) <= a_lim and z >= z1 and z >= z0 then 117 // tee th in the gap , not h i t t i n g the wa l l bounds , c l u t c h in p o s i t i o n 118 eng_state = 1 ; 119 t = 0 ; 120 mass ∗ der ( zv ) = f_spring_n_current − s t i f f 2 ∗ ( z − z1 ) ; 121 e l s e i f z < z0 then 122 // tee th o u t s i d e gap 123 eng_state = 0 ; 124 t = 0 ; II A. Clutch Model 125 mass ∗ der ( zv ) = f_spring_n_current ; 126 else 127 eng_state = 0 ; 128 t = 0 ; 129 mass ∗ der ( zv ) = 0 ; 130 end i f ; 131 e l s e i f engage_req == 0 and prev_eng_state == 1 then 132 // Detatch c l u t c h . Clutch engaged in prev ious s t a t e 133 i f abs ( a ) > a_lim and z >= z0 then 134 // tee th in the gap , h i t t i n g the wa l l bounds 135 eng_state = 1 ; 136 t = s t i f f ∗ ( abs ( a ) − a_lim ) ∗ s i g n ( a ) + WallBounceDamping ∗ w; 137 mass ∗ der ( zv ) = f_spring_n_current − WallScrapeDamp ∗ ( z − z0 ) ∗ zv ; 138 e l s e i f abs ( a ) <= a_lim and z >= z0 then 139 // tee th in the gap , not h i t t i n g the wa l l bounds 140 eng_state = 1 ; 141 t = 0 ; 142 mass ∗ der ( zv ) = f_spring_n_current ; 143 e l s e i f z < z0 then 144 // c l u t c h was engaged but now has somehow reached o u t s i d e dog tee th 145 eng_state = 0 ; 146 t = 0 ; 147 mass ∗ der ( zv ) = f_spring_n_current ; 148 else 149 eng_state = 0 ; 150 t = 0 ; 151 mass ∗ der ( zv ) = 0 ; 152 end i f ; 153 e l s e i f engage_req == 0 and prev_eng_state == 0 then 154 // Detatch c l u t c h . 155 i f z < z0 and z >= 0 then 156 // c l u t c h not engaged , i . e . o u t s i d e dog tee th 157 eng_state = 0 ; 158 t = 0 ; 159 mass ∗ der ( zv ) = f_spring_n_current ; 160 e l s e i f z < z0 and z < 0 then 161 // c l u t c h not engaged 162 eng_state = 0 ; 163 t = 0 ; 164 mass ∗ der ( zv ) = f_spring_n_current − DampingBel l ev i l l e_extra ∗ zv ; 165 e l s e i f z >= z0 then 166 // tee th buncing o f eachother 167 eng_state = 0 ; 168 t = 0 ; 169 mass ∗ der ( zv ) = f_spring_n_current − s t i f f 2 ∗ ( z − z0 ) ; 170 else 171 eng_state = 0 ; 172 t = 0 ; 173 mass ∗ der ( zv ) = 0 ; 174 end i f ; 175 else 176 eng_state = 0 ; 177 t = 0 ; 178 mass ∗ der ( zv ) = 0 ; 179 end i f ; 180 end c l u t c h ; III B Hybrid DAE Listing B.1 – SimCode gernerated by OpenModelica for the case study 1 engage_req=i f cur rent > 0 .01 then 1 else 0 [ I n t e g e r ] 2 f_spring_n_current=KI ∗ cur rent + (−k_spring ) ∗ z − DampingBe l l ev i l l e ∗ zv [ Real ] 3 a=0.02777777777777778 ∗ s i n (36 . 0 ∗ phi ) [ Real ] 4 DER.z=zv [ Real ] 5 DER.phi=w[ Real ] 6 prev_eng_state=pre ( eng_state ) [ I n t e g e r ] 7 DER.zv=i f engage_req == 1 and prev_eng_state == 0 then i f z < 0 .0016 then DIVISION( f_spring_n_current , mass ) else i f z >= 0 .0016 and 8 abs (w) > 3 .141592653589793 then DIVISION( f_spring_n_current − s t i f f 2 ∗ (−0 .0016 + z ) , mass ) else i f z >= 0 .0016 and abs (w) < 3 .141592653589793 9 and abs ( a ) <= 0 .004363309284746571 then DIVISION( f_spring_n_current , mass ) else i f z >= 0 .0016 and abs (w) < 3 .141592653589793 and abs ( a ) > 10 0 .004363309284746571 then DIVISION( f_spring_n_current − s t i f f 2 ∗ (−0 .0016 + z ) , mass ) else 0 . 0 else i f engage_req == 1 and prev_eng_state == 1 11 then i f abs ( a ) > 0 .004363309284746571 and z < 0 .0032 and z >= 0 .0016 then DIVISION( f_spring_n_current − WallScrapeDamp ∗ (−0 .0016 + z ) ∗ zv , mass ) 12 else i f abs ( a ) > 0 .004363309284746571 and z >= 0 .0032 and z >= 0 .0016 then DIVISION( f_spring_n_current − s t i f f 2 ∗ (−0 .0032 + z ) − WallScrapeDamp ∗ 13 (−0 .0016 + z ) ∗ zv , mass ) else i f abs ( a ) <= 0 .004363309284746571 and z < 0 .0032 and z >= 0 .0016 then DIVISION( f_spring_n_current , mass ) else i f 14 abs ( a ) <= 0 .004363309284746571 and z >= 0 .0032 and z >= 0 .0016 then DIVISION( f_spring_n_current − s t i f f 2 ∗ (−0 .0032 + z ) , mass ) else i f z < 0 .0016 15 then DIVISION( f_spring_n_current , mass ) else 0 . 0 else i f engage_req == 0 and prev_eng_state == 1 then i f abs ( a ) > 0 .004363309284746571 and z >= 16 0 .0016 then DIVISION( f_spring_n_current − WallScrapeDamp ∗ (−0 .0016 + z ) ∗ zv , mass ) else i f abs ( a ) <= 0 .004363309284746571 and z >= 0 .0016 then 17 DIVISION( f_spring_n_current , mass ) else i f z < 0 .0016 then DIVISION( f_spring_n_current , mass ) else 0 . 0 else i f engage_req == 0 and prev_eng_state 18 == 0 then i f z < 0 .0016 and z >= 0 . 0 then DIVISION( f_spring_n_current , mass ) else i f z < 0 .0016 and z < 0 . 0 then DIVISION( f_spring_n_current − 19 DampingBel l ev i l l e_extra ∗ zv , mass ) else i f z >= 0 .0016 then DIVISION( f_spring_n_current , mass ) else 0 . 0 else 0 . 0 [ Real ] 20 21 t=i f engage_req == 1 and prev_eng_state == 0 then i f z < 0 .0016 then 0 . 0 else i f z >= 0 .0016 and abs (w) > 3 .141592653589793 then 22 HiSpeedDamping2 ∗ w else i f z >= 0 .0016 and abs (w) < 3 .141592653589793 and abs ( a ) <= 0 .004363309284746571 then 0 . 0 else i f z >= 0 .0016 and 23 abs (w) < 3 .141592653589793 and abs ( a ) > 0 .004363309284746571 then LoSpeedDamping2 ∗ w else 0 . 0 else i f engage_req == 1 and prev_eng_state == 1 24 then i f abs ( a ) > 0 .004363309284746571 and z < 0 .0032 and z >= 0 .0016 then WallBounceDamping ∗ w + s t i f f ∗ (−0 .004363309284746571 + abs ( a ) ) 25 ∗ /∗ Real ∗/ ( s i g n ( a ) ) else i f abs ( a ) > 0 .004363309284746571 and z >= 0 .0032 and z >= 0 .0016 then WallBounceDamping ∗ w + s t i f f ∗ 26 (−0 .004363309284746571 + abs ( a ) ) ∗ /∗ Real ∗/ ( s i g n ( a ) ) else 0 . 0 else i f engage_req == 0 and prev_eng_state == 1 then i f abs ( a ) > 27 0 .004363309284746571 and z >= 0 .0016 then WallBounceDamping ∗ w + s t i f f ∗ (−0 .004363309284746571 + abs ( a ) ) ∗ /∗ R