Automated model-based testing of hybrid systems

In automated model-based input-output conformance testing, tests are automati- cally generated from a speci¯cation and automatically executed on an implemen- tation. Input is applied to the implementation and output is observed from the implementation. If the observed output is allowed according to the test, then test- ing may continue, or stop with the verdict pass. If the observed output is not allowed according to the test, then testing stops with the verdict fail. The advantages of this test method are that: ² specifications can be reused to test every product in exactly the same way, ² test environments can be controlled because the behavior of the environment is specified as the input of the implementation, ² tests can be generated that a test engineer did not think of yet, ² a huge quantity of tests can be generated and repeated endlessly, and ² the test engineer can focus on testing the parts of the system for which tests are not automated. A hybrid system is a system with both discrete-events and continuous behavior. By continuous behavior we usually mean the behavior of physical quantities over time. A thermostat that observes a chamber temperature and turns on a heater based on the observed temperature change is a system with continuous input and discrete-event output. A robot arm that moves with a certain speed on command (e.g. "GO LEFT") is a system with discrete-event input and continuous output. Within the Tangram project, a four year research project on model-based test and integration methods and their applications, one of the goals was to develop model- based testing for hybrid systems. This involves incorporating continuous behavior and discrete-event behavior into one input-output conformance relation and into a notion of hybrid test. Then, this approach to hybrid model-based testing had to be tried out in practice, in an industrial environment. In this thesis we describe the result of this research. In Chapter 2 and Chapter 3 we define the necessary preliminaries for defining our conformance relation and notion of test for hybrid systems. We use hybrid tran- sition systems to formally represent the implementation and the specification of a system. We base our conformance relation on the discrete-event input-output con- formance relation by Tretmans, and the timed input-output conformance relations by Brandan-Briones and Brinksma, and by Krichen and Tripakis. In Chapter 4 we define our input-output conformance relation for hybrid systems. In this chapter we also define a notion of test for hybrid systems that we have proven sound and exhaustive with respect to the hybrid conformance relation. Based on the notion of hybrid test, we have implemented a proof-of-concept hybrid model-based test tool. The architecture of our tool is based on the TorX test tool and the tests are generated from a hybrid specification using the hybrid  simulation tool. In Chapter 5 we describe TorX and the hybrid X language. In Chapter 6 we describe the issues involved in developing a hybrid model-based test tool in general, and our proof-of-concept tool in particular. In order to better fit theory and practice, we adapt our hybrid input-output conformance relation and notion of test to a conformance relation and notion of test for sampled behavior. We have proven that, under certain conditions, if a hybrid implementation conforms to a hybrid specification, then the implementation also conforms to the specification with sampled behavior. In Chapter 7 we describe the results of a case study that we have performed on a vacuum controller of a waferstepper machine. This controller has sampled con- tinuous input (namely samples of pressure observations) and discrete-event output (namely controlling pumps and valves). We have made a specification that models the sequences of events required for pumping down a vacuum chamber or venting a vacuum chamber. We have modeled the pressure loow in the chamber as continu- ous behavior. With the proof-of-concept tool we have been able to generate tests, stimulate the vacuum control software with sampled pressure low, observe output of the vacuum control software, and give a verdict. We have found a fault in the control software that was not found previously in the field, nor by co-simulation of the controller and a model of the hardware, nor by model checking using Uppaal. This result shows that hybrid model-based testing has added value. In chapter 8 we describe the results of this research and we present some directions for future research.