Checking Timed Bisimulation with Bounded Zone-History Graphs

Lars Luthmann, Hendrik Göttmann and Malte Lochau

Abstract

Timed automata (TA) are a well-established formalism for discrete-state/continuous-time behaviors of time-critical reactive systems. Concerning the fundamental analysis problem of comparing a candidate implementation against a specification, both given as TA, it has been shown that timed trace equivalence is undecidable, whereas timed bisimulation equivalence is decidable. The corresponding proof utilizes region graphs, a finite, but very space-consuming characterization of TA semantics. In practice, most TA tools use zone graphs instead, a symbolic and generally more efficient representation of TA semantics, to automate analysis tasks. However, zone graphs only produce sound results for analysis tasks being reducible to plain reachability problems thus being too imprecise for checking timed bisimilarity. To the best of our knowledge, no practical tool is currently available for automated timed bisimilarity-checking. In this paper, we propose bounded zone-history graphs, a novel characterization of TA semantics facilitating an adjustable trade-off between precision and scalability of timed-bisimilarity checking. Our approach supports non-deterministic timed automata with silent moves. We further present experimental results gained from applying our tool TimBrCheck to a collection of community benchmarks, providing insights into trade-offs between precision and efficiency.

Technical Report

The technical report containing all proofs is available at arXiv.org.

Using the Tool

Download our tool and the case studies here: link (ZIP archive)

Please note that our tool was compiled with Azul OpenJDK 13.0.1 but it may be run with previous versions of Java. However, if you encounter any problems during execution, please update your Java installation to the latest release.

The tool implementation of our approach is evaluated by means of the five case studies av-protocol, collision-avoidance, gear-control, ieee-rcp, train-gate-controller. There is a folder for each of the five case studies in the ZIP archive, containing the TA of the case study and all corresponding mutants.

The tool (tioa-tool.jar) is invoked from the command line. The following is an example call for the check of timed bisimulation on the RCP case study and one of its mutants.

java -Xmx2048M -Xss4m -jar tioa-tool.jar -b 30 ieee-rcp/ieee-rcp.xml ieee-rcp/ieee-rcp-reset-1.xml

The corresponding files for the TA of the case studies are ieee-rcp/ieee-rcp.xml and ieee-rcp/ieee-rcp-reset-1.xml, respectively. The parameter b specifies the bound for the zone histories (30 in this example). A short summary of the execution is printed to the console after finishing the check for bisimilarity.

Kontakt

Technische Universität Darmstadt

Fachbereich Elektrotechnik und Informationstechnik

Fachgebiet Echtzeitsysteme

Prof. Dr. rer. nat. Andy Schürr

Magdalenenstr. 4

64289 Darmstadt

+49(0)6151 16-22350

+49(0)6151 16-22352

Drucken | Impressum | Datenschutzerklärung | Sitemap | Suche | Kontakt
Zum SeitenanfangZum Seitenanfang