Measuring with timed patterns
27th International Conference on Computer Aided Verification, CAV 2015, California, Amerika Birleşik Devletleri, 18 - 24 Temmuz 2015, cilt.9207, ss.322-337, (Tam Metin Bildiri)
- Yayın Türü: Bildiri / Tam Metin Bildiri
- Cilt numarası: 9207
- Doi Numarası: 10.1007/978-3-319-21668-3_19
- Basıldığı Şehir: California
- Basıldığı Ülke: Amerika Birleşik Devletleri
- Sayfa Sayıları: ss.322-337
- Boğaziçi Üniversitesi Adresli: Hayır
Özet
We propose a declarative measurement specification language for quantitative performance evaluation of hybrid (discrete-continuous) systems based on simulation traces. We use timed regular expressions with events to specify patterns that define segments of simulation traces over which measurements are to be taken. In addition, we associate measure specifications over these patterns to describe a particular type of performance evaluation (maximization, average, etc.) to be done over the matched signal segments. The resulting language enables expressive and versatile specification of measurement objectives. We develop an algorithm for our measurement framework, implement it in a prototype tool, and apply it in a case study of an automotive communication protocol. Our experiments demonstrate that the proposed technique is usable with very low overhead to a typical (computationally intensive) simulation.