Tese de Doutorado: 08/04/2011, 09:00.

postado em 8 de abr de 2011 06:43 por Hyggo Oliveira de Almeida
Aluno: Wilkerson Andrade
Título: Symbolic Model-Based Testing for Real-Time Systems
Local: Auditório do CEEI. 
Banca Examinadora: Prof. Patrícia Machado (UFCG), Orientadora, Prof. Tiago Massoni (UFCG),  Prof. Rohit Gheyi (UFCG), Prof. Augusto Sampaio (UFPE), Prof. David Deharbe (UFRN). 
Data: 08/04/2011. 
Hora: 09:00. 

Resumo: 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 traffic 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 financial, environmental or human areas. As the costs and consequences of failures can be high, formal verification 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 interesting in the search for methods, techniques and tools to support the testing of real-time systems. Testing real-time systems 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 finite 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 finite 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..

Agradecemos a sua presença.