Dvlab Open WikiTicc (Tool for Interface Compatibility and Composition) is a tool for the prototyping and verification of distributed designs. Ticc provides the following features:
Modeling of design components, and of their interaction.
- Each component can specify both its behavior, and the behavior it expects from other components.
- Modeling capabilities include shared state (via shared and private variables), one- and bi-directional communication and synchronization (via synchronization actions).
Benefit: concise, natural modeling of asynchronous systems with shared state and flexible communication patterns.
Composition and compatibility checking.
- When components are composed, Ticc checks that they interact correctly.
- Ticc is capable of propagating the input constraints of components upon composition.
Benefit: the consistency of the design is assured.
Simulation and Verification.
- Ticc can check CTL properties of designs, as well as simulate them.
- Ticc relies on symbolic methods for the efficient analysis of large state spaces.
Benefit: the correctness of designs with respect to specifications can be checked.
Ticc is in constant development, and we periodically release versions with additional capabilities. If you are interested in some capability not currently supported, let us know by email. Also, if you want to implement some capabilities yourself, we will try to facilitate your work as we can.
Downloading, Installing, and Using Ticc
The most recent release of Ticc is Ticc 0.3, released on May 15, 2008.
Requirements:
Operating systems: linux, or Windows under Cygwin. Let us know if you get it working under Mac OS X.
Software: a C compiler, and Ocaml 3.08 (it will most likely not work with Ocaml 3.06, and it has been reported to work with Ocaml 3.09).
Release Information: Features added in the various releases of Ticc.
Ticc is released under the GPL v.2; for details, see the COPYING file.
Ticc Foundations: the theoretical and technical foundations of Ticc.
Further reading: this bibliography contains a list of papers and other readings that are relevant to Ticc.
Feedback, Feature Requests, Bugs
Bugs: if you find a bug, please email us, including if possible the .si and .in files, along with any relevant output.
For developers only: These pages are viewable only by people in the DvlabFriendsGroup.
Task List: a list of tasks for the Ticc team.
Future Extensions: a discussion on future extensions to Ticc.
Developer Talk: a forum for discussion among Ticc developers.
Authors
The current developers of Ticc are Luca de Alfaro, Bo Adler, Marco Faella, Axel Legay, Vishwanath Raman, and Pritam Roy. Past contributors include Leandro Dias Da Silva.
Other Tools for Interfaces
The following other tools are available for interface formalisms:
Chic: Checker for Interface Compatibility, developed at UC Berkeley by Thomas A. Henzinger, Arindam Chakrabarti, and others, is a tool for synchronous interfaces.
Ptolemy also contains an implementation of Interface Automata.
If you know of additional tools, please email us.
Financial Support
The TICC project has been partially supported by:
- NSF CAREER award CCR-0132780
- NSF grant CCR-0234690
- ONR grant N00014-02-1-0671
- ARP awards TO.030.MM.D and TO.030.2MM.D
Visitors to the group have also been supported by the following grants:
- F.R.I.A Grant
- Awards from Brazilian government agencies CNPq and CAPES