Abstract
In formal testing, the assumption of input enabling is typically made. This assumption requires all inputs to be enabled anytime. In addition, the useful concept of quiescence is sometimes applied. Briefly, a system is in a quiescent state when it cannot produce outputs.
In this paper, we relax the input enabling assumption, and allow some input sets to be enabled while others remain disabled. Moreover, we also relax the general bound M used in timed systems to detect quiescence, and allow different bounds for different sets of outputs.
By considering the tiocoM theory, an enriched theory for timed testing with repetitive quiescence, and allowing the partition of input sets and output sets, we introduce the mtiocoM relation. A test derivation procedure which is nondeterministic and parameterized is further developed, and shown to be sound and complete wrt mtiocoM .
Original language | Undefined |
---|---|
Title of host publication | Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005 |
Editors | K.K. Lau, R. Banach |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 264-279 |
Number of pages | 16 |
ISBN (Print) | 3 540 29797 9 |
DOIs | |
Publication status | Published - Nov 2005 |
Event | 7th International Conference on Formal Engineering Methods, ICFEM 2005 - Manchester, United Kingdom Duration: 1 Nov 2005 → 4 Nov 2005 Conference number: 7 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Volume | 3785 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 7th International Conference on Formal Engineering Methods, ICFEM 2005 |
---|---|
Abbreviated title | ICFEM |
Country/Territory | United Kingdom |
City | Manchester |
Period | 1/11/05 → 4/11/05 |
Keywords
- EWI-1631
- IR-54947
- METIS-229701