Testing multi input-output real-time systems

L. Brandan Briones, Hendrik Brinksma

  • 13 Citations

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 languageUndefined
Title of host publicationFormal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005
EditorsK.K. Lau, R. Banach
Place of PublicationBerlin
PublisherSpringer Verlag
Pages264-279
Number of pages16
ISBN (Print)3 540 29797 9
DOIs
StatePublished - Nov 2005
Event7th International Conference on Formal Engineering Methods, ICFEM 2005 - Manchester, United Kingdom

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume3785
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Conference on Formal Engineering Methods, ICFEM 2005
Abbreviated titleICFEM
CountryUnited Kingdom
CityManchester
Period1/11/054/11/05

Fingerprint

Testing

Keywords

  • EWI-1631
  • IR-54947
  • METIS-229701

Cite this

Brandan Briones, L., & Brinksma, H. (2005). Testing multi input-output real-time systems. In K. K. Lau, & R. Banach (Eds.), Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005 (pp. 264-279). (Lecture Notes in Computer Science; Vol. 3785). Berlin: Springer Verlag. DOI: 10.1007/11576280_19

Brandan Briones, L.; Brinksma, Hendrik / Testing multi input-output real-time systems.

Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005. ed. / K.K. Lau; R. Banach. Berlin : Springer Verlag, 2005. p. 264-279 (Lecture Notes in Computer Science; Vol. 3785).

Research output: Scientific - peer-reviewConference contribution

@inbook{84803c40b5a249338e016f930ff3b632,
title = "Testing multi input-output real-time systems",
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 .",
keywords = "EWI-1631, IR-54947, METIS-229701",
author = "{Brandan Briones}, L. and Hendrik Brinksma",
note = "eemcs1633",
year = "2005",
month = "11",
doi = "10.1007/11576280_19",
isbn = "3 540 29797 9",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "264--279",
editor = "K.K. Lau and R. Banach",
booktitle = "Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005",

}

Brandan Briones, L & Brinksma, H 2005, Testing multi input-output real-time systems. in KK Lau & R Banach (eds), Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005. Lecture Notes in Computer Science, vol. 3785, Springer Verlag, Berlin, pp. 264-279, 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, United Kingdom, 1-4 November. DOI: 10.1007/11576280_19

Testing multi input-output real-time systems. / Brandan Briones, L.; Brinksma, Hendrik.

Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005. ed. / K.K. Lau; R. Banach. Berlin : Springer Verlag, 2005. p. 264-279 (Lecture Notes in Computer Science; Vol. 3785).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Testing multi input-output real-time systems

AU - Brandan Briones,L.

AU - Brinksma,Hendrik

N1 - eemcs1633

PY - 2005/11

Y1 - 2005/11

N2 - 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 .

AB - 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 .

KW - EWI-1631

KW - IR-54947

KW - METIS-229701

U2 - 10.1007/11576280_19

DO - 10.1007/11576280_19

M3 - Conference contribution

SN - 3 540 29797 9

T3 - Lecture Notes in Computer Science

SP - 264

EP - 279

BT - Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005

PB - Springer Verlag

ER -

Brandan Briones L, Brinksma H. Testing multi input-output real-time systems. In Lau KK, Banach R, editors, Formal Methods and Software Engineering: 7th International Conference on Formal Engineering Methods, ICFEM 2005. Berlin: Springer Verlag. 2005. p. 264-279. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/11576280_19