Henry, L; Jéron, T; Markey, N; (2022) Control strategies for off-line testing of timed systems. Formal Methods in System Design , 60 pp. 147-194. 10.1007/s10703-022-00403-w.

Preview

Text article.pdf - Accepted Version Download (728kB) | Preview

Abstract

Partial observability and controllability are two well-known issues in test-case synthesis for reactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. We extend a previous approach to this problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that try to minimize both cooperations of the system and distance to the satisfaction of a test purpose or to the next cooperation, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method. We finally propose a symbolic algorithm to compute those strategies.

Download activity - last month

Export as JSONXMLCSV

Download activity - last 12 months

Export as CSVXMLJSON

Downloads by country - last 12 months

Export as JSONXMLCSV

Archive Staff Only

View Item