### Abstract

Original language | Undefined |
---|---|

Title of host publication | Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013) |

Editors | Margus Veanes, Luca Viganò |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 214-231 |

Number of pages | 18 |

ISBN (Print) | 978-3-642-38915-3 |

DOIs | |

Publication status | Published - Jun 2013 |

Event | 7th International Conference on Tests & Proofs 2013 - Budapest, Hungary Duration: 18 Jun 2013 → 19 Jun 2013 Conference number: 7 http://www.spacios.eu/TAP2013/ |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 7942 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 7th International Conference on Tests & Proofs 2013 |
---|---|

Abbreviated title | TAP 2013 |

Country | Hungary |

City | Budapest |

Period | 18/06/13 → 19/06/13 |

Internet address |

### Keywords

- EC Grant Agreement nr.: FP7/2007-2013
- EC Grant Agreement nr.: FP7/318490
- EWI-23427
- Quiescence
- IR-86479
- IOCO
- Divergence
- METIS-297694
- Model-Based Testing

### Cite this

*Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013)*(pp. 214-231). (Lecture Notes in Computer Science; Vol. 7942). Berlin: Springer. https://doi.org/10.1007/978-3-642-38916-0_13

}

*Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013).*Lecture Notes in Computer Science, vol. 7942, Springer, Berlin, pp. 214-231, 7th International Conference on Tests & Proofs 2013, Budapest, Hungary, 18/06/13. https://doi.org/10.1007/978-3-642-38916-0_13

**Divergent quiescent transition systems.** / Stokkink, W.G.J.; Timmer, Mark; Stoelinga, Mariëlle Ida Antoinette.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Divergent quiescent transition systems

AU - Stokkink, W.G.J.

AU - Timmer, Mark

AU - Stoelinga, Mariëlle Ida Antoinette

N1 - eemcs-eprint-23427

PY - 2013/6

Y1 - 2013/6

N2 - Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that no output is produced in certain states. 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 or not to allow this behaviour. To explicitly model quiescence in all its glory, we introduce Divergent Quiescent Transition Systems (DQTSs). DQTSs model quiescence using explicit delta-labelled transitions, analogous to Suspension Automata (SAs) in the well-known ioco framework. Whereas SAs have only been defined implicitly, DQTSs for the first time provide a fully-formalised framework for quiescence. Also, while SAs are restricted to convergent systems (i.e., without tau-cycles), we show how quiescence can be treated naturally using a notion of fairness, allowing systems exhibiting divergence to be modelled as well. We study compositionality under the familiar automata-theoretical operations of determinisation, parallel composition and action hiding. We provide a non-trivial algorithm for detecting divergent states, and discuss its complexity. Finally, we show how to use DQTSs in the context of model-based testing, for the first time presenting a full-fledged theory that allows ioco to be applied to divergent systems.

AB - Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that no output is produced in certain states. 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 or not to allow this behaviour. To explicitly model quiescence in all its glory, we introduce Divergent Quiescent Transition Systems (DQTSs). DQTSs model quiescence using explicit delta-labelled transitions, analogous to Suspension Automata (SAs) in the well-known ioco framework. Whereas SAs have only been defined implicitly, DQTSs for the first time provide a fully-formalised framework for quiescence. Also, while SAs are restricted to convergent systems (i.e., without tau-cycles), we show how quiescence can be treated naturally using a notion of fairness, allowing systems exhibiting divergence to be modelled as well. We study compositionality under the familiar automata-theoretical operations of determinisation, parallel composition and action hiding. We provide a non-trivial algorithm for detecting divergent states, and discuss its complexity. Finally, we show how to use DQTSs in the context of model-based testing, for the first time presenting a full-fledged theory that allows ioco to be applied to divergent systems.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/318490

KW - EWI-23427

KW - Quiescence

KW - IR-86479

KW - IOCO

KW - Divergence

KW - METIS-297694

KW - Model-Based Testing

U2 - 10.1007/978-3-642-38916-0_13

DO - 10.1007/978-3-642-38916-0_13

M3 - Conference contribution

SN - 978-3-642-38915-3

T3 - Lecture Notes in Computer Science

SP - 214

EP - 231

BT - Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013)

A2 - Veanes, Margus

A2 - Viganò, Luca

PB - Springer

CY - Berlin

ER -