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.
[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,
[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,
[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,
[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