TRIO:
formal language, method and tools
Introduction
A selection of publications about TRIO
Industrial experiences
TRIO Tools
Ongoing research
People involved
Related sites
Introduction
TRIO (Tempo Reale ImplicitO) is a formal language and a method for the
specification, analysis
and verification of critical, real-time systems. The TRIO language is
based on a metric extension of first-order temporal logic and exploits
typical
object-oriented features to support the managing of large, complex, and
maintainable
specifications. A collection of protoptype tools
supporting the editing
of
TRIO specifications, their formal analysis, and the derivation of test
cases
therefrom is available free of charge. TRIO has been used successfully
in
several industrial projects and is still the object of our ongoing
research
activity. Among the TRIO publications listed here, [4, 10, 11] provide
an introduction
to the language and its application (for a very quick introduction to
the TRIO language you can refer to this document).
Recently, higher-order features have been introduced in TRIO, which resulted
in a TRIO sibling, Higher-Order TRIO (HOT for short).
HOT, with respect to TRIO, allows users to quantify variables whose type corresponds
to a HOT class, a feature that makes HOT a very powerful and expressive
language.
Go to a selection of publications about TRIO
Industrial experiences: a
selection of reports
- Ciapessoni E., Coen-Porisini A., Crivelli E., Mandrioli D.,
Mirandola P., Morzenti A., From
formal models to formally-based methods:
an industrial experience, ACM Transactions on Software
Engineering and
Methodology, vol. 8. no 1, January 1999, pp.79-113 download.
- Basso M., Ciapessoni E., Crivelli E., Mandrioli D., Morzenti A.,
Ratto E., San Pietro P., A
logic-based approach to the specification and
design
of the control system of a pondage power plant, in C.Tully
(editor)
Improving
Software Practice: Case Experiences, John Wiley & Sons, Series in
Software
Based Systems, pp. 79-96, 1998.
- Gargantini A., Liberati L., Morzenti A., Zacchetti C.,
Specifying, Validating, and testing
a Traffic Management System in the TRIO environment,
Proceedings of COMPASS, 11th Annual Conference on Computer Assurance, June 1996
pp. 65-76 download.
- Basso M., Ciapessoni E., Crivelli E., Mandrioli D., Morzenti A.,
Ratto E., San Pietro P., Experimenting
a Logic-Based Approach to the
Specification and Design of the Control System of a Pondage Power Plant,
Proceedings
of the ICSE-17 Workshop on Formal Methods Application in Software
Engineering Practice, 1995, pp. 174-181
- Mandrioli D., Morzenti A., Specifica
in TRIO delle Unità di Elaborazione Periferica: aspetti relativi
alla struttura delle versioni, alla gestione della base dei tempi e al
conteggio dei quanti di energia (in italian), Technical report,
Dipartimento di Elettronica ed Informazione, November 1997 download.
Tools &
Prototypes (use at your own risk)
Old stuff
Go to an overview of ongoing research on TRIO and formal models and methods
People
Related sites
Page last updated September 6th,
2005.
TRio
Integrated Development EnvironmeNT (TRIDENT)