Testing multi input-output real-time systems (Extended Version)

L. Brandan Briones, Hendrik Brinksma

Research output: Book/ReportReport

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.
LanguageUndefined
Place of PublicationEnschede
PublisherFormal Methods and Tools (FMT)
Number of pages20
StatePublished - Sep 2005

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
No.TR-CTIT-05-40
ISSN (Print)1381-3625

Keywords

  • EWI-5729
  • METIS-248101
  • IR-57037

Cite this

Brandan Briones, L., & Brinksma, H. (2005). Testing multi input-output real-time systems (Extended Version). (CTIT Technical Report Series; No. TR-CTIT-05-40). Enschede: Formal Methods and Tools (FMT).
Brandan Briones, L. ; Brinksma, Hendrik. / Testing multi input-output real-time systems (Extended Version). Enschede : Formal Methods and Tools (FMT), 2005. 20 p. (CTIT Technical Report Series; TR-CTIT-05-40).
@book{7430d5894cba418ca6bfc84c4d1cc526,
title = "Testing multi input-output real-time systems (Extended Version)",
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-5729, METIS-248101, IR-57037",
author = "{Brandan Briones}, L. and Hendrik Brinksma",
note = "Imported from CTIT",
year = "2005",
month = "9",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Formal Methods and Tools (FMT)",
number = "TR-CTIT-05-40",

}

Brandan Briones, L & Brinksma, H 2005, Testing multi input-output real-time systems (Extended Version). CTIT Technical Report Series, no. TR-CTIT-05-40, Formal Methods and Tools (FMT), Enschede.

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

Enschede : Formal Methods and Tools (FMT), 2005. 20 p. (CTIT Technical Report Series; No. TR-CTIT-05-40).

Research output: Book/ReportReport

TY - BOOK

T1 - Testing multi input-output real-time systems (Extended Version)

AU - Brandan Briones,L.

AU - Brinksma,Hendrik

N1 - Imported from CTIT

PY - 2005/9

Y1 - 2005/9

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-5729

KW - METIS-248101

KW - IR-57037

M3 - Report

T3 - CTIT Technical Report Series

BT - Testing multi input-output real-time systems (Extended Version)

PB - Formal Methods and Tools (FMT)

CY - Enschede

ER -

Brandan Briones L, Brinksma H. Testing multi input-output real-time systems (Extended Version). Enschede: Formal Methods and Tools (FMT), 2005. 20 p. (CTIT Technical Report Series; TR-CTIT-05-40).