Publications‎ > ‎Doctoral Theses‎ > ‎


 Title Symbolic Model-Based Testing for Real-Time Systems
 Author Wilkerson de Lucena Andrade
 Download PDF
  Doctoral Thesis, Computer Science, Federal University of Campina Grande, April 2011.
 Abstract Real-time systems are the ones whose correct behaviour depends not only on the generated results but also on whether the results are generated at the right time-points. Real-time systems are used in different contexts such as monitoring of patients in hospitals, air trafc control systems, and embedded systems in robots, appliances, vehicles, and so on. For these systems, dependability is an important property that demands rigorous application of V & V activities, since defects can mean losses in nancial, environmental or human areas. As the costs and consequences of failures can be high, formal verication and model checking have been used in the V & V process. However, as these approaches have practical limitations, testing is also used as a complementary approach since it allows the execution of real scenarios within execution environments. Consequently, there is a growing interest in the search for methods, techniques and tools to support the testing of real-time systems, which poses a number of distinguishing challenges such as implementations composed of parallel activities with synchronous and asynchronous events (interruptions), with different deployment architectures, and resource limitation and time constraints on the execution environment. This thesis focuses on model-based conformance testing of real-time systems. In this context, current approaches are mostly based either on nite state machines/transition systems or on timed automata. However, most real-time systems manipulate data while being subject to time constraints. The usual solution consists in enumerating data values (in nite domains) while treating time symbolically, thus leading to the classical state explosion problem. This thesis proposes a new model of real-time systems as an extension of both symbolic transition systems and timed automata, in order to handle both data and time requirements symbolically. We propose a conformance testing theory to deal with this model and describe a test case generation process based on a combination of symbolic execution and constraint solving for the data part and symbolic analysis for timed aspects. Moreover, the proposed approach can deal with interruption testing. Finally, two case studies were performed in order to evaluate the practical application of the proposed approach.