156
A. Cimatti et al.
own phase transitions. In turn, these subsidiary systems may require transitions
to occur in systems subsidiary to them and so on.
Traditionally, the integration of these distributed transition targets are validated via simulation and testing, which while sufficient to reach a desired design
performance are labor and time intensive. Having a more efficient process for
arriving at and validating a set of design targets that satisfy the overall system requirements is clearly beneficial in these contexts. Firstly, we would like
to verify that these requirements prevent failed transitions in which the time
performance of the subsidiary systems lead to outcomes where our main system (e.g., the power generation system) cannot perform a transition within its
time window. For example, suppose the power system has a time window within
which it must transition from low-power mode to high-power mode; in order for
it to achieve this transition, however, it requires that two subsidiary systems,
a cooling system and a fuel supply system, must themselves transition from a
low-output mode to a high-output mode, each within their own target transition
time windows. If these time windows are not compatible, the power generator
may fail to provide the high power in time. Secondly, if our starting set of requirements is inadequate to provide this guarantee, we would like to be able to
synthesize a set of requirements that is adequate to this task.
In this paper, we formalize the problem starting from a simple industrially
relevant setting, where the components have a linear sequence of phases, must
progress to the next phase within a certain interval of time, and must respect
some dependencies upon the phases of other components. Dependencies are expressed as Boolean combinations of variables representing the component phases
and are divided into two types: (i) signal dependencies, where the entering of a
component into a phase is conditioned by the presence of other components in
some specific phases; (ii) state dependencies, where a component can stay in a
phase only if, during all its stay, other components are in some specific phases.
We are interested in the following problems: 1) checking if the requirements are
compatible, i.e., if all reachable states can be extended with an execution satisfying the requirements; thus, if the components satisfy the local requirements,
they cannot lead the system to an illegal state (where a component does not
receive the input in time); 2) checking if the requirements are consistent, i.e.,
there exists an execution of the components satisfying all requirements (inconsistency is actually a pathological case of incompatibility); 3) synthesizing the
set of refinements (same requirements with stricter intervals) that are consistent and compatible. We show how the first two verification problems can be
naturally translated into a model checking problem for timed automata with
shared variables. Exploiting the linear structure of the requirements, we propose
an encoding of the problem into SMT. If all intervals are bounded, the encoding
is quantifier-free. Finally, both approaches have been extended to solve also the
synthesis problem, using synthesis for parametrized model checking of TAs and
quantifier elimination in SMT, respectively.
We implemented the SMT-based approach in a tool called TRICker and carried out experimental evaluation, comparing it with other tools for the verifica-
A. Cimatti et al.
own phase transitions. In turn, these subsidiary systems may require transitions
to occur in systems subsidiary to them and so on.
Traditionally, the integration of these distributed transition targets are validated via simulation and testing, which while sufficient to reach a desired design
performance are labor and time intensive. Having a more efficient process for
arriving at and validating a set of design targets that satisfy the overall system requirements is clearly beneficial in these contexts. Firstly, we would like
to verify that these requirements prevent failed transitions in which the time
performance of the subsidiary systems lead to outcomes where our main system (e.g., the power generation system) cannot perform a transition within its
time window. For example, suppose the power system has a time window within
which it must transition from low-power mode to high-power mode; in order for
it to achieve this transition, however, it requires that two subsidiary systems,
a cooling system and a fuel supply system, must themselves transition from a
low-output mode to a high-output mode, each within their own target transition
time windows. If these time windows are not compatible, the power generator
may fail to provide the high power in time. Secondly, if our starting set of requirements is inadequate to provide this guarantee, we would like to be able to
synthesize a set of requirements that is adequate to this task.
In this paper, we formalize the problem starting from a simple industrially
relevant setting, where the components have a linear sequence of phases, must
progress to the next phase within a certain interval of time, and must respect
some dependencies upon the phases of other components. Dependencies are expressed as Boolean combinations of variables representing the component phases
and are divided into two types: (i) signal dependencies, where the entering of a
component into a phase is conditioned by the presence of other components in
some specific phases; (ii) state dependencies, where a component can stay in a
phase only if, during all its stay, other components are in some specific phases.
We are interested in the following problems: 1) checking if the requirements are
compatible, i.e., if all reachable states can be extended with an execution satisfying the requirements; thus, if the components satisfy the local requirements,
they cannot lead the system to an illegal state (where a component does not
receive the input in time); 2) checking if the requirements are consistent, i.e.,
there exists an execution of the components satisfying all requirements (inconsistency is actually a pathological case of incompatibility); 3) synthesizing the
set of refinements (same requirements with stricter intervals) that are consistent and compatible. We show how the first two verification problems can be
naturally translated into a model checking problem for timed automata with
shared variables. Exploiting the linear structure of the requirements, we propose
an encoding of the problem into SMT. If all intervals are bounded, the encoding
is quantifier-free. Finally, both approaches have been extended to solve also the
synthesis problem, using synthesis for parametrized model checking of TAs and
quantifier elimination in SMT, respectively.
We implemented the SMT-based approach in a tool called TRICker and carried out experimental evaluation, comparing it with other tools for the verifica-