Safe Decomposition of Startup Requirements
169
Fig. 4: Comparison on the bounded category (consistency checking on the first
row and compatibility checking on the second).
scalability than ParamIC3, though there are several instances for which synthesis
via quantifier elimination is still very expensive.
6 Conclusions
In this paper, we defined verification and synthesis problems of industrial relevance focused on the decomposition of startup requirements into local timing
constraints and dependencies on components. Namely, we addressed the problem
of checking if the local requirements are free of integration errors (i.e., consistent and compatible), and the problem of synthesizing the region of refinements
of the original specification that are error free. The problem can be naturally
translated into model checking and synthesis problems for timed automata with
shared variables. Exploiting the structure of the requirements, we provide an
encoding into SMT where consistency and incompatibility correspond to satisfiability queries, while synthesis is resolved by means of quantifier elimination.
In the future, we will consider various directions, such as extending the applicability of the approach to more general structures with loops, enriching the
synthesis problem with cost functions to repair the specification driven by specific industrial goals, and considering more complex representations of signals
exchanged between components.
169
Fig. 4: Comparison on the bounded category (consistency checking on the first
row and compatibility checking on the second).
scalability than ParamIC3, though there are several instances for which synthesis
via quantifier elimination is still very expensive.
6 Conclusions
In this paper, we defined verification and synthesis problems of industrial relevance focused on the decomposition of startup requirements into local timing
constraints and dependencies on components. Namely, we addressed the problem
of checking if the local requirements are free of integration errors (i.e., consistent and compatible), and the problem of synthesizing the region of refinements
of the original specification that are error free. The problem can be naturally
translated into model checking and synthesis problems for timed automata with
shared variables. Exploiting the structure of the requirements, we provide an
encoding into SMT where consistency and incompatibility correspond to satisfiability queries, while synthesis is resolved by means of quantifier elimination.
In the future, we will consider various directions, such as extending the applicability of the approach to more general structures with loops, enriching the
synthesis problem with cost functions to repair the specification driven by specific industrial goals, and considering more complex representations of signals
exchanged between components.