Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

5-2017

Abstract

Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions occurring in a finite time), which is unrealistic. We show here that synthesizing parameter valuations such that at least one counterexample run is non-Zeno is undecidable for parametric timed automata (PTAs). Still, we propose a semi-algorithm based on a transformation of PTAs into Clock Upper Bound PTAs to derive all valuations whenever it terminates, and some of them otherwise.

Keywords

Automata theory, Formal methods, Interactive computer systems, NASA, Real time systems

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, May 16-18: Proceedings

Volume

10227

First Page

35

Last Page

51

ISBN

9783319572871

Identifier

10.1007/978-3-319-57288-8_3

Publisher

Springer

City or Country

Cham

Additional URL

https://doi.org/10.1007/978-3-319-57288-8_3

Download

Share

COinS