Ongoing research on TRIO and on formal models and methods in general

Foreword (intended audience)
On the TRIO language and formal models in general
On formal methods and methodologies (mostly TRIO-based)
On verification and validation techniques and tools
On the application of formal models and methods to real-life systems

Foreword (intended audience)

This page presents an overview of the research on formal models and methods that is currently being developed in our group.
It is mostly directed to two categories of people:
The page lists the main topics we are currently working on and, for each topic, the people who are involved in that research.

On the TRIO language and formal models in general
(system modeling)

Formal models for Software Architectures
(TC and ArchiTRIO)

This research effort is aimed at developing suitable, logic-based formalisms for modeling application architectures in terms of their interacting software components.
The formalisms must be able to describe not only the structure of the system (the number and type of its components and their interfaces), but also the behavior of its parts and the dynamic of their interactions.
Unlike in notations such as UML, though, the goal here is to avoid using separate languages to describe the different aspects of structure and behavior of the application, but to have a unique, logic-based notation which is suitable to model all facets of the system under development.
However, compatibility with UML is an important design goal for the formalisms that we develop. As UML is the de facto standard for application modeling in the software world (and it is now also being applied to domains other than software development), it cannot be ignored, and part of our research effort focuses on enriching (rather than replacing) the informal, imprecise UML notation with the precise concepts of our logic-based formalisms.
This research draws from past experience with the TRIO/CORBA (TC) language [22], but the target language (called ArchiTRIO[1, 2]) is more general, and is not restricted to modeling CORBA applications.
The logic foundations of the ArchiTRIO approach are, much like in the TC case, rooted in the TRIO formal language; as a consequence, ArchiTRIO is suitable for describing both general-puropose and real-time systems, but is not restricted to either case.

People principally involved: Alberto Coen-Porisini, Dino Mandrioli, Angelo Morzenti, Matteo Pradella, Matteo Rossi, Pierluigi San Pietro

Integration and composition of formal models and methods

The acceptance of formal methods in the practice of software engineering requires them to be fully scalable and usable not only on small "toy" examples, but also on industrial-strength projects.
Compositional methods are those that bring modularization techniques to formal analysis processes, thus allowing the scalability of the analysis. Research in this area specifically considers how to devise scalability techniques, with TRIO as the reference formal language. More precisely, this requires both technical and methodological aspects to be considered. Furthermore, the methods should be given an adequate tool support, extending the other TRIO capabilities (see the section on tools).
A further step to permit a true scalability of formal languages is the ability to integrate specifications written using different formal languages, and to consequently verify such heterogeneous specifications. Research in this area aims at putting different formal languages on a common ground, thus giving a formal meaning to a multi-language specification. The integration considers obviously technical aspects, such as the integration of languages with different underlying semantics and the composition of properties expressed in different formalisms. Furthermore, integration also considers methodological aspects: on the one hand, we should not lessen the effectiveness of each of the methods being integrated by unnaturalizing their use; on the other hand we should be able to guide the integration process under a unifying synthetic view.

People principally involved: Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, Matteo Rossi

Formal models for security

This work is aimed at developing formalisms (mostly logic-based) for building models that take into account diverse aspects of system (and in particular network) security. While most of the formal approaches to security are targeted at modeling protocols (for example for establishing a secure channel between two computers, or for authentication of users in a domain, etc.) the goal of this research is more general, and involves (at least in principle) all security aspects of a system (from user authentication to secure information exchange, to network vulnerabilities, etc.).
The ultimate goal of this research is to allow users to build models that allow a variety of analyses: determine if a network is vulnerable to certain attacks (and, if the network is vulnerable, where), or if it is possible that a user of a system gains priviliges he/she should not have, or if there can be leakage of sensitive information, and so on.

People principally involved: Dino Mandrioli, Matteo Pradella, Matteo Rossi, Pierluigi San Pietro



On formal methods and methodologies (mostly TRIO-based)
(system development)

Refinement: from formal specifications to formal designs

TRIO was initially developed as a formalism for system specification, but has also been used as the basis for formal languages for modeling the architecture of an application.
This research effort aims at giving a formal definition of what constitutes the refinement of a TRIO specification in a TRIO-based architecture, and also at developing a method for deriving formal architectures from TRIO specifications. It is mostly based on our past research efforts documented in [22] and [21].

People principally involved: Alberto Coen-Porisini, Dino Mandrioli, Matteo Pradella, Matteo Rossi

Deriving formal TRIO-based models from semi-formal UML descriptions
(The ArchiTRIO method)

UML is a very popular and widely used notation for modeling software (and not only) systems. However, its lack of precision and informal semantics hamper its usability for precise analysis. This research is aimed at defining a methodology to derive formal, TRIO-based models from semi-formal UML ones.
The effort is twofold.
On one side, a mapping between some UML concepts (mostly, but not only, from class diagrams) and TRIO elements is defined. The mapping is deterministic, and can be performed automatically by a translator.
On the other side, the aforementioned mapping between UML and TRIO cannot be complete, as UML is only semi-formal, and most of the semantics carried by UML diagrams is in fact intimately tied to the user's understanding of the model. Then, methodological steps are needed to aid and complete the automatic translation with the information lacking in the diagram itself. Part of this research focuses on devising such methodology, which allows users to obtain a fully formal model from the initial semi-formal one.

People principally involved: Dino Mandrioli, Matteo Pradella, Matteo Rossi, Giordano Sassaroli (CEFRIEL)



On verification and validation techniques and tools

TRIDENT: The TRIO IDE

TRIDENT (TRio Integrated Development ENvironmenT) is an eclipse-based environment for writing and analyzing TRIO-based models. It allows users to build TRIO models, and launch analysis plugins and tools. It also supports (or will support) the methods and methodologies described above and, in particular, the UML-to-TRIO traslation.

People principally involved: Dino Mandrioli, Matteo Pradella, Matteo Rossi, Giordano Sassaroli (CEFRIEL)

Model checking with TRIO

We propose a novel application on model checking through SPIN as a means for verifying purely descriptive (or hybrid descriptive/operational) specifications written in TRIO. The approach is based on the translation of TRIO formulae into Promela programs guided by an equivalence between TRIO and alternating Büchi automata, as documented in [17].


People principally involved: Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini

Theorem proving with TRIO
(not only PVS)

An encoding of the TRIO logic in the PVS theorem prover is already available ([19]). However, there is ample room for improvement in the supporting proving strategies. This research effort will then focus on making the existing TRIO-specific PVS strategies better, so as to relieve as much proving burden from the user as possible.
In addition, theorem provers other than PVS will be explored, for example ACL2.

People principally involved: Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, Matteo Pradella, Matteo Rossi



On the application of formal models and methods to real-life systems (case studies)

Formal methods applied to the design of manufacturing systems

There are a number of areas in which the use of formal methods is still unexplored, but which could greatly benefit from their application as a complement, rather than substitute, to existing modeling and analysis techniques. One such area is Flexible Manufacturing Systems (FMS), which are production systems composed of computer numerically controlled (CNC) machining centers that process prismatic metal components. For FMSs, simulation is the most widely-used analysis method when it comes to deciding if a certain system configuration, scheduling policy, etc. is suitable to achieve the desired productivity goals. However, great insights can be gained by using (logic-based) formal methods next to simulation tools, for example to decide if a set of scheduling (but not only) rules will always guarantee that a certain deadline for the completion of the production process is met, or to determine the ranges in which certain parameters must range in order to be able to reach some desired target, and so on.
[28] lays out some ideas and presents some initial results in this area of research.

People principally involved: Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, Matteo Rossi, Pierluigi San Pietro


Page last updated September 29th, 2004.