User-Friendly Formal Methods
(for Time-Critical Systems)

Summary

In software-intensive systems software parts interact with a variety of physical phenomena and devices to reach global goals. Software-intensive systems are typically embedded, often have dependability requirements, and might be safety-critical with real-time constraints.
The design of dependable (and safety-critical) systems, in particular, requires great care and precision, as errors in their development can lead to potentially dire consequences. It can greatly benefit from the use of formal methods, whose sound mathematical foundations permit, at least in principle, to employ formal verification techniques to analyze the properties (e.g. correctness) of the system under development.
In practice, the application of formal methods still requires considerable skills and know-how on the part of the developer, which often hinders their acceptance in the industrial community. In addition, for systems that exhibit significant time-related properties (such as, for example, embedded and real-time systems), the temporal dimension adds to the difficulties [FMMR08], as "classic", software-only development methods (even formal ones) are hardly designed to deal with time-related issues in a natural manner.
The goal of this research topic is to develop tool-supported formal design techniques which, while retaining the sound mathematical foundations typical of formal methods, provide users with primitives with which they are likely more familiar.
In fact, the more user-friendly a formal method, the less its users will realize they are employing a formal method to begin with. In other words, the most user-friendly formal method is the one that is entirely hidden from its users, the one that disappears in the development process (while permeating it). Making formal methods invisible to their users is crucial when one considers that, as software applications infiltrate more and more aspects of our everyday life (the "disappearing computer" phenomenon), the notion of "developer" becomes broader and broader. This leads to envision scenarios in which even people with no technical training at all develop (e.g., by recombining existing parts in novel ways) software-intensive systems, even ones with dependability requirements. Providing this whole new class of developers of software-based dependable systems with formal design techniques that they can use without even realizing it is a challenge that this research topic intends to address.

Possible outline of the approach

Design techniques in general, and formal ones in particular, typically have two facets: modeling, and analysis (verification). To make formal methods more appealing (that is, user-friendly) to the industrial community, one can act on either aspect, or both at the same time.
From the point of view of modeling, different directions can be pursued. A first possibility is to combine formal notations with non-formal (or semi-formal) ones adopted as industry standards (e.g. UML and its profiles).This is the approach adopted in the ArchiTRIO language [PRM05], which combines the formal approach of the TRIO temporal logic with (a subset of) the aforementioned UML notation.
A second, complementary possibility is to allow users to employ different formal modeling paradigms (e.g. temporal logics, Petri Nets, Timed Automata) to describe different (possibly overlapping) aspects of the system under development, while at the same time maintaining the consistency among the various parts and views. A preliminary example of this approach is presented in [FPR08b].

From the point of view of verification, enhanced user-friendliness is synonymous with, on the one hand, higher automation, and, on the other hand, broader range of applicability. Recent improvements in the average performance of SAT-solvers have made SAT-based approaches to formal verification very appealing and promising. Zot [PMS07] is a fully automated SAT-based tool which permits to formally verify models described in metric temporal logic (using a discrete notion of time). While promising, the approach has limitations in terms of the size of the problems that can be analyzed and in their scope (i.e. what classes of systems can be verified). Various techniques can be investigated to overcome these limitations.
Abstraction and compositional techniques (e.g. [FRMM07]) are typical approaches that are used to overcome the limitation in size. Discretization techniques [FPR08a] have been employed in the past to broaden the scope of applicability of the Zot tool to continuous-time systems. Other approaches that have been pursued to broaden the scope of the Zot tool consist in endowing it with operational constructs [PMS08] and primitives to model timed automata [FPR08b].

Finally, a formal method, to be user-friendly (and usable in practice) must be supported by suitable tools, which facilitate the modeling and verification activities at the core of the design technique.

While the works cited above constitute a starting point towards "the user-friendly formal method", they are just that, i.e., the beginning. In particular, making the modeling notation more user-friendly (i.e. endowing it with powerful primitives that permit to describe rich properties), and making the verification technique user-friendly (i.e. making it more automated), can be conflicting goals. In fact, powerful modeling primitives usually call for great expressive power in the formal modeling notation. However, there is a well-known trade-off between expressiveness and amenability to automated verification: the greater the expressive power, the lower the degree of automation of the associated verification techniques.

The ultimate goal of this research topic is to push formality and user-friendliness to their respective limits: to make formal methods at the same time central to the development of software-intensive systems and disappear in it.

References:

[FMMR08] Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, Matteo Rossi, Modeling Time in Computing: a taxonomy and a comparative survey, accepted for publication (pending minor revisions) in ACM Computing Surveys. (A preliminary version of the paper can be found in the Technical Report 2007.22, Dipartimento di Elettronica ed Informazione)

[FPR08a] Carlo A. Furia, Matteo Pradella, Matteo Rossi, Automated Verification of Dense-Time MTL Specifications via Discrete-Time Approximation, International Symposium on Formal Methods, Lecture Notes in Computer Science, vol. 5014, May 2008, pp. 132-147, doi:10.1007/978-3-540-68237-0_11

[FPR08b] Carlo A. Furia, Matteo Pradella, Matteo Rossi, Practical Automated Partial Verification of Multi-Paradigm Real-Time Models, International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, October 2008, to appear (An extended version of the paper can be found in the Technical Report arXiv.org > cs > 0804.4383)

[FRMM07] Carlo A. Furia, Matteo Rossi, Dino Mandrioli, Angelo Morzenti, Automated Compositional Proofs for Real-Time Systems, Theoretical Computer Science, vol. 376, n. 3, May 2007, pp. 164-184, doi:10.1016/j.tcs.2007.02.003

[PMS07] Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro, The Symmetry of the Past and of the Future: Bi-Infinite Time in the Verification of Temporal Properties, ESEC/SIGSOFT FSE, Sptember 2007, pp. 312-320, doi:10.1145/1287624.1287669

[PMS08] Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro, Refining Real-Time System Specifications through Bounded Model- and Satisfiability Checking, International Conference on Automated Software Engineering, September 2008, to appear

[PRM05] Matteo Pradella, Matteo Rossi, Dino Mandrioli, ArchiTRIO: a UML-compatible language for architectural description and its formal semantics, Formal Techniques for Networked and Distributed Systems, Lecture Notes in Computer Science, vol. 3731, October 2005, pp. 381-395 doi:10.1007/11562436_28


Contacts:

Dino Mandrioli (mandrioli AT elet.polimi.it)
Angelo Morzenti (morzenti AT elet.polimi.it)
Matteo Pradella (pradella AT elet.polimi.it)
Matteo Rossi (rossi AT elet.polimi.it)

Page last modified July 2nd, 2008.