Controlling Actions and Time in Parametric Timed Automata
Étienne André, Michał Knapik, Wojciech Penczek, Laure Petrucci · 2016
Cyber-physical systems involve both discrete actions and real-time that elapses depending on timing constants. In this paper, we introduce a formalism for such systems containing both real-time parameters in linear timing constraints and switchable (Boolean) actions. We define a new approach for synthesizing combinations of parameter valuations and allowed actions, under which the system correctness is ensured when expressed in the form of a safety property. We apply our approach to a railway crossing system example with a malicious intruder potentially threatening the system safety.