Safe Decomposition of Startup Requirements:
Verification and Synthesis
Alessandro Cimatti
1 , Luca Geatti
1,2 , Alberto Griggio
1 , Greg Kimberly
3 ,
and Stefano Tonetta
1
1 Fondazione Bruno Kessler, Trento, Italy
cimatti@fbk.eu, lgeatti@fbk.eu, griggio@fbk.eu, tonettas@fbk.eu
2 University of Udine, Udine, Italy
luca.geatti@uniud.it
3 The Boeing Company, Seattle, USA
greg.kimberly@boeing.com
Abstract. The initialization of complex cyber-physical systems often
requires the interaction of various components that must start up with
strict timing requirements on the provision of signals (power, refrigeration, light, etc.). In order to safely allow an independent development
of components, it is necessary to ensure a safe decomposition, i.e. the
specification of local timing requirements that prevent later integration
errors due to the dependencies.
We propose a high-level formalism to model local timing requirements
and dependencies. We consider the problem of checking the consistency
(existence of an execution satisfying the requirements) and compatibility (absence of an execution that reaches an integration error) of the
local requirements, and the problem of synthesizing a region of timing
constraints that represents all possible correct refinements of the original specification. We show how the problems can be naturally translated
into a model checking and synthesis problem for timed automata with
shared variables. Exploiting the linear structure of the requirements, we
propose an encoding of the problem into SMT. We evaluate the SMTbased approach using MathSAT and show how it scales better than the
automata-based approach using Uppaal and nuXmv.
1 Introduction
Complex industrial cyber-physical systems often have an initialization procedure
that requires to reach a startup mode within a specified design target time interval. In order for the system as a whole to complete the startup within the
required interval, each subcomponent of the system may have to go through a
number of intermediate phases, within their own target intervals, each of which
may itself be dependent upon other subcomponents reaching startup or intermediate phases. E.g. for a power generation system to startup at full power, it may
need to transition first through a low power output phase and a number of subsidiary systems (perhaps cooling or fuel supply) may first have to undergo their
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 155–172, 2020.
https://doi.org/10.1007/978-3-030-45190-5 9
Verification and Synthesis
Alessandro Cimatti
1 , Luca Geatti
1,2 , Alberto Griggio
1 , Greg Kimberly
3 ,
and Stefano Tonetta
1
1 Fondazione Bruno Kessler, Trento, Italy
cimatti@fbk.eu, lgeatti@fbk.eu, griggio@fbk.eu, tonettas@fbk.eu
2 University of Udine, Udine, Italy
luca.geatti@uniud.it
3 The Boeing Company, Seattle, USA
greg.kimberly@boeing.com
Abstract. The initialization of complex cyber-physical systems often
requires the interaction of various components that must start up with
strict timing requirements on the provision of signals (power, refrigeration, light, etc.). In order to safely allow an independent development
of components, it is necessary to ensure a safe decomposition, i.e. the
specification of local timing requirements that prevent later integration
errors due to the dependencies.
We propose a high-level formalism to model local timing requirements
and dependencies. We consider the problem of checking the consistency
(existence of an execution satisfying the requirements) and compatibility (absence of an execution that reaches an integration error) of the
local requirements, and the problem of synthesizing a region of timing
constraints that represents all possible correct refinements of the original specification. We show how the problems can be naturally translated
into a model checking and synthesis problem for timed automata with
shared variables. Exploiting the linear structure of the requirements, we
propose an encoding of the problem into SMT. We evaluate the SMTbased approach using MathSAT and show how it scales better than the
automata-based approach using Uppaal and nuXmv.
1 Introduction
Complex industrial cyber-physical systems often have an initialization procedure
that requires to reach a startup mode within a specified design target time interval. In order for the system as a whole to complete the startup within the
required interval, each subcomponent of the system may have to go through a
number of intermediate phases, within their own target intervals, each of which
may itself be dependent upon other subcomponents reaching startup or intermediate phases. E.g. for a power generation system to startup at full power, it may
need to transition first through a low power output phase and a number of subsidiary systems (perhaps cooling or fuel supply) may first have to undergo their
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 155–172, 2020.
https://doi.org/10.1007/978-3-030-45190-5 9