2005/01/01 by Kim G. Larsen, Larsen, Kim G., Marius Mikučionis +3
Computer Science · #Formal Methods in Verification #Online testing #Software Reliability and Analysis Research #Software Testing and Debugging Techniques #black-box testing #embedded systems #mo #real-time systems #relativized timed input/output conformance #symbolic state representation
paper · doi:10.4230/dagsemproc.04371.3
openalex publication_date 2005/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present TUPPAAL --- a new tool for online black-box testing of real-time embedded systems from non-deterministic timed automata specifications. We describe a sound and complete randomized online testing algorithm, and describe how to implement it using symbolic state representation and manipulation techniques. We propose the notion of relativized timed input/output conformance as the formal implementation relation. A novelty of this relation and our testing algorithm is that they explicitly take environment assumptions into account, generate, execute and verify the result online using the UPPAAL on-the-fly model-checking tool engine. A medium size case study shows promising results in terms of error detection capability and computation performance.