Quiescent transition systems

Stokkink, Gerjan (2012) Quiescent transition systems.

[img]
Preview
PDF
648kB
Abstract:Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that, in certain system states, no output is provided by the system. The notion of quiescence is also essential to model-based testing: if a particular implementation under test does not provide any output, then the test evaluation algorithm must decide whether to allow this behaviour, or not. A Suspension Automaton (SA) is a kind of labelled transition system in which observations of quiescence are explicitly represented with special �-transitions. SAs form the basic building block on which the well-known ioco model-based testing framework is based. The SA model, however, has a number of aws. First of all, a SA is not de�ned as an entity in itself, and cannot be built from scratch. Secondly, its properties have not been fully investigated yet. Thirdly, and most importantly, the SA model does not allow nondeterminism or divergence to occur, thereby limiting the number of systems that can be naturally modelled. To address these limitations, we introduce in this thesis the socalled Quiescent Transition Systems (QTSs), which form a fully formalised alternative to the existing SAs. We also introduce Divergent Quiescent Transition Systems (DQTSs), a more complex variant on QTSs which allow (state-�nite) divergence to occur. We show how QTSs and DQTSs can be created from existing generic models by an operation called delta�cation. Furthermore, we de�ne the three familiar automata-theoretical operations of determinisation, parallel composition and action hiding for these models, and show that (D)QTSs are closed under these operations. Additionally, we prove that the operation of delta�cation is commutative with all of these operations. Finally, we provide an evaluation in which we compare QTS, DQTSs and SAs. We illustrate that in the context of test-based modelling, the use of (D)QTSs o�ers several advantages over SAs, and recommend that the ioco theory be reformulated in terms of the (D)QTS model.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:http://purl.utwente.nl/essays/61938
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page