TRio Integrated Development EnvironmeNT
TRIDENT (short for TRio Integrated Development EnvironmeNT) is a tool
for the development and analysis of time-critical systems based on the TRIO formal language.
TRIDENT is based on the eclipse
platform, and is currently being developed jointly by Politecnico di Milano and CEFRIEL.
The environment is still in a prototypical stage, so many of the
intended features are still incomplete. With TRIDENT one can (or will
be able to):
Currently, TRIDENT supports editing modular TRIO specifications and
history check single TRIO classes. A prototype TRIO model checker based
on the SPIN tool is currently being
integrated in the environment. In addition, a prototype plugin capable
of partially transforming XMI files into TRIDENT objects has been
developed and is available in the TRIDENT disribution.
- write complex formal specifications in TRIO;
- transform semi-formal UML specifications in TRIO ones;
- check the compatibility of execution traces with TRIO
specifications (in TRIO terms, perfrom history checking);
- model check TRIO specifications;
- perform theorem proving on TRIO models;
- generate test cases from TRIO specifications.
Here is a snapshot of the tool, showing a simple TRIO class:
TRIDENT is freely available to those who are interested in using it.
To install TRIDENT, all you have to do is download one of the following
then unzip and untar the files in a directory of preference. To launch
the IDE (preset with the appropriate default plugin), simply run the
"eclipse(.exe)" executable in the "eclipse" subdirectory.
As mentioned above, TRIDENT is still in its infancy, so it is in
continuous evolution. Updates of the TRIDENT plugins for the eclipse platform will be posted on
this page, so if you are interested in trying out the tool, please
check this page from time to time for updates.
To install updates, simply substitute the directories included in the
updates with the corresponding ones on your hard drive, then (re)start
If you have any comments, remarks, suggestions, or if you have any bugs
to report, feel free to send an email here.
Page last updated May 5th,