We have implemented ECDAR that is a new tool for compositional design and
verification of real time systems. In ECDAR, a component interface describes
both the behavior of the component and the component’s assumptions about the
environment. The tool, which is based in a timed extension of the interface
theory provided by Henzinger and de Alfaro, supports the important operations
of a good compositional reasoning theory: composition, conjunction, quotient,
consistency/satisfaction checking, and refinement. The operators can be used to
combine basic models into larger specifications to construct comprehensive
system descriptions from basic requirements. Algorithms to perform these
operations have been based on a game theoretical setting that permits, for
example, to capture the real-time constraints on communication events between
components. The compositional approach allows for scalability in the
verification.

ECDAR is the first tool that implements the theory of timed interfaces with
composition, conjunction, and refinement. Hence the tool provides a complete
methodology for the design of timed systems. The tool comes with a nice user
interface which makes it usable by non specialists. In addition, the tool
proposes a quotient operation to synthesize a timed component.

Website: www.cs.aau.dk/~adavid/ecdar/index.html