TRIO: formal language, method and tools

A selection of publications about TRIO
Industrial experiences
TRIO Tools
Ongoing research
People involved
Related sites


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

  1. 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.
  2. 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.
  3. 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.
  4. 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
  5. 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


Related sites

Page last updated September 6th, 2005.