Benchmarks for hybrid systems verification. (English) Zbl 1135.93324

Fehnker, Ansgar; Ivančić, Franjo

Alur, Rajeev (ed.) et al., Hybrid systems: computation and control. 7th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25–27, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21259-0/pbk). Lecture Notes in Computer Science 2993, 326-341 (2004).

Summary: There are numerous application examples for hybrid systems verification in recent literature. Most of them were introduced to illustrate a new approach to hybrid systems verification, and are therefore of a limited size. Others are case studies that serve to prove that an approach can be applied to real world problems. Verification of these typically requires a lot of domain experience to obtain a tractable, verifiable model. Verification of a case study yields a singular result that is hard to compare and time-consuming to reproduce.
This paper introduces three benchmarks for hybrid systems verification. These benchmarks are independent from a particular approach to verification, they have a limited domain, and have a simple basic structure. Nevertheless, these benchmarks can be scaled to arbitrary complexity, and offer the possibility to inject phenomena that are known to be problematic in hybrid verification. This paper presents result for a first set of instances, as an example of how these benchmark can be used to compare different tools and approaches.
For the entire collection see [Zbl 1046.93002].

MSC:

93B30	System identification
93C30	Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93B40	Computational methods in systems theory (MSC2010)

Keywords:

system identification; benchmark characteristics

Software:

Uppaal