Safe Decomposition of Startup Requirements
157
tion of timed automata. We used Uppaal [6] and nuXmv [7] to model check TAs
and MathSAT [12] to solve the SMT problems. We performed an experimental
evaluation based on a test-set of randomly generated local requirements. When
comparing the SMT-based approach with the automata-based one, the results
highlight a better performance of the former technique on all three problems.
Related Work The problem of the integration and compatibility of input/output
timed automata has been extensively studied in the literature. Typically, works
in the literature focus on deadlock checking (see, e.g., [4,5]). The work of [2] also
addresses the parameter synthesis to avoid deadlocks in timed automata. In order
to check for livelocks, liveness properties can be addressed with approaches proposed in [10,7]. A general definition of illegal states for timed interface automata
is given in [13]. As shown in the extended version of the paper the compatibility problem addressed in this paper can be seen as a subcase of the homonym
problem for input/output timed interface automata. As we are considering a
closed system, the problem reduces to the existence of a deadlock or livelock in
a phase of some component (depending if the related time interval is bounded
or not). Moreover, compared to the above model checking approaches we are
considering a specific fragment of timed automata with a linear structure that
can be exploited for specialized solutions.
Related problems have been addressed in the context of task scheduling. In
the formalism introduced in [16,17], called DRT (short for digraph real-time task
model), in which tasks and deadlines are expressed as directed graphs, the problem of determining whether a schedule exists (feasibility problem) bears some
similarities with the consistency checking problem we study here. The DRT
model allows the use of very general graph topologies, with multiple outgoing
branches and loop-backs, but it does not consider dependencies across different
tasks. The main difference with our work is that the problem is addressed from
a global point of view (i.e., the existence of a global scheduler that can coordinate the execution of the tasks), whereas we are interested in local solutions,
in which each requirement can be considered in isolation. Another difference is
the approach used to tackle the problem: while in [16] dynamic programming is
used to deal with the possible explosion of the search space, we use SMT [14] as
the main framework for all the three above-mentioned problems.
Outline. In Sec. 2, we introduce a suitable formalism to model local requirements and we formalize the three problems. In Sec. 3, we propose the reductions
of compatibility checking and consistency checking into TAs and SMT. The corresponding solutions for the synthesis problem are then described in Sec. 4. The
experimental results are described in Sec. 5. In Sec. 6, we draw some conclusions
and highlight possible future directions of this work.
2 Problem Statement
Domain formalization We propose a high level formalism to model the local
requirements.
157
tion of timed automata. We used Uppaal [6] and nuXmv [7] to model check TAs
and MathSAT [12] to solve the SMT problems. We performed an experimental
evaluation based on a test-set of randomly generated local requirements. When
comparing the SMT-based approach with the automata-based one, the results
highlight a better performance of the former technique on all three problems.
Related Work The problem of the integration and compatibility of input/output
timed automata has been extensively studied in the literature. Typically, works
in the literature focus on deadlock checking (see, e.g., [4,5]). The work of [2] also
addresses the parameter synthesis to avoid deadlocks in timed automata. In order
to check for livelocks, liveness properties can be addressed with approaches proposed in [10,7]. A general definition of illegal states for timed interface automata
is given in [13]. As shown in the extended version of the paper the compatibility problem addressed in this paper can be seen as a subcase of the homonym
problem for input/output timed interface automata. As we are considering a
closed system, the problem reduces to the existence of a deadlock or livelock in
a phase of some component (depending if the related time interval is bounded
or not). Moreover, compared to the above model checking approaches we are
considering a specific fragment of timed automata with a linear structure that
can be exploited for specialized solutions.
Related problems have been addressed in the context of task scheduling. In
the formalism introduced in [16,17], called DRT (short for digraph real-time task
model), in which tasks and deadlines are expressed as directed graphs, the problem of determining whether a schedule exists (feasibility problem) bears some
similarities with the consistency checking problem we study here. The DRT
model allows the use of very general graph topologies, with multiple outgoing
branches and loop-backs, but it does not consider dependencies across different
tasks. The main difference with our work is that the problem is addressed from
a global point of view (i.e., the existence of a global scheduler that can coordinate the execution of the tasks), whereas we are interested in local solutions,
in which each requirement can be considered in isolation. Another difference is
the approach used to tackle the problem: while in [16] dynamic programming is
used to deal with the possible explosion of the search space, we use SMT [14] as
the main framework for all the three above-mentioned problems.
Outline. In Sec. 2, we introduce a suitable formalism to model local requirements and we formalize the three problems. In Sec. 3, we propose the reductions
of compatibility checking and consistency checking into TAs and SMT. The corresponding solutions for the synthesis problem are then described in Sec. 4. The
experimental results are described in Sec. 5. In Sec. 6, we draw some conclusions
and highlight possible future directions of this work.
2 Problem Statement
Domain formalization We propose a high level formalism to model the local
requirements.