Dependability in software-intensive
systems can be achieved only through
the application of solid design principles. That, in turn, is achieved through
an understanding of the product and
specialization of engineers in particular domains, product types, and techniques. Abstract interpretation can aid
in reducing the complexity inherent in
proving properties and correctness of
complex software systems, which otherwise would not be feasible. Such an approach facilitates automated reasoning
and fully automated reasoning. In particular, recent advances in verification
techniques have made it possible to
verify concurrent systems and prove termination by considering termination of
a thread without considering concurrency per se.
In the realm of formal methods, too,
we encounter radical and normal engineering, as well as the whole spectrum
of intermediate phases in between. In a
sense, the ratio of radical design to normal design can be taken as a measure of
the maturity of a field of engineering.
In retrospect, radical engineering of, and with, formal methods has
characterized the first 20 years of this
field, making it an art: it was limited
to a restricted scope of few users and a
few high-budget, high-risk projects for
which high assurance was compelling.
This is no longer the case today:
˲ A first transition from weak to
strong formal methods17 moved the
field from specification-only toward
tool-based semantics analysis, making
formal methods not only descriptive
but also operational.
˲ A second transition shifted tool support from heavyweight to lightweight
formal methods: from proof assistants,
which still require specialist skills, education, and a good deal of intuition, to
fully automatic analyses embedded in a
software engineer’s usual development
This shift is central to enabling every software developer to use the techniques seamlessly, advancing from a
radical design endeavor to everyday
practice. Then it is not an art anymore,
just another craft, in the same way that
photography enabled everybody to portray a subject with perfect faithfulness
to the subject’s traits, at a very reasonable cost and without being, or resort-
ing to, a portrait painter.
We observe that today different techniques occupy different positions on
this transition axis. While termination
proof of concurrent systems is still an art
(a case for radical design), techniques
such as type checking are enforced by
the vast majority of programming environments (natural design), and many
other techniques are walking the naturalization path. It is a steep and narrow
path that takes decades to follow. For
example, abstract interpretation was
discovered in the 1970s, but it is only in
recent years that we have had tools such
as Astrée to enable normal developers
to apply collections of sophisticated abstract interpretations as part of their daily routine within an enhanced normal
engineering process. Model checking,
rewarded this year with the ACM A.M.
Turing Award to Edmund M. Clarke,
Joseph Sifakis, and E. Allen Emerson,
is another successful example of formal
methods that became increasingly natural in the course of their 25+ years of
history. Once naturalized, the magic of
a technique (and of its gurus) vanishes,
but we all profit from the achievements
of the revolutionaries that enter mainstream production.
As noted 12 years ago, specialization
in high-assurance systems concerns
devising appropriate heterogeneous
methods that adequately exploit the
various application-specific characteristics of the problem. 16 Computer-aided method engineering is the new craft.
It targets understanding and solving
problems heterogeneously at a meta
level, where whole methods and paradigms are combined. Even though this
holds already for many sequential systems, it is particularly true for distributed systems, which by their nature are of
a much higher conceptual complexity.
Multicore architectures in our laptops
and massively multicore systems as part
of Web computing and cloud computing environments demand increased
This quest continues…
1. Bowen, J.P. and Hinchey, M.G. Seven more myths of
formal methods. IEEE Software 12, 4 (July 1995),
2. Bowen, J.P. and Hinchey, M.G. High-integrity system
specification and design. Formal Approaches to
Computing and Information Technology. Springer-Verlag, London, 1999.
3. Cook, B., Podelski, A., Rybalchenko, A. Termination
proofs for systems code. In Proceedings of the
2006 ACM SIGPLAN Conference on Programming
Language Design and Implementation, 415–426.
4. Cook, B., Podelski, A., Rybalchenko, A. Proving
thread termination. In Proceedings of the 2007 ACM
SIGPLAN Conference on Programming Language
Design and Implementation, PLDI 2007, 320–330.
5. Cousot. P. and Cousot, R. Systematic design of
program analysis frameworks. In Conf. rec. 6th
Annual ACM SIGPLAN-SIGAC T Symp. on Principles
of Prog. Lang., ACM Press (1979), pp 269–282.
6. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné,
A., Monniaux, D., and Rival, X. Varieties of static
analyzers: A comparison with Astrée. In Proceedings
of the 1st IEEE & IFIP Int. Symp. on Theoretical
Aspects of Software Engineering, TASE ’07. IEEE
Computer Society Press (2007), 3–17.
7. Delmas, D. and Souyris, J. Astrée: From research to
industry. Lecture Notes in Computer Science 4634,
Springer (2007), 437–451.
8. Ferdinand, C., Heckmann, R., and Wilhelm, R.
Analyzing the worst-case execution time by abstract
interpretation of executable code. Lecture Notes in
Computer Science 4147, Springer (2006), 1–14.
9. Gotsman, A., Berdine, J., Cook, B., Sagiv, M. Thread-modular shape analysis. In Proceedings of the
2007 ACM SIGPLAN Conference on Programming
Language Design and Implementation, 266–277.
10. Gray, J. Dependability in the Internet era. In
Proceedings of the High Dependability Computing
Consortium Conference, Santa Cruz, CA, May 7, 2001.
11. Hall, J.A. Seven myths of formal methods. IEEE
Software 7, 5 (Sept. 1990), 11–19.
12. Laprie, J.-C., ed. Dependability: Basic concepts and
terminology in English, French, German, Italian and
Japanese. Dependable Computing and Fault- Tolerant
Systems, Vol. 5, Springer-Verlag, NY, 1992.
13. Patterson, D. et al. recovery Oriented Computing
(rOC): Motivation, Definition, Techniques, and Case
Studies. Computer Science Technical Report UCB//
CSD-02-1175. University of California, Berkeley, CA,
March 15, 2002.
16. Steffen, B., Margaria, T. Method engineering for real-life concurrent systems. ACM Computing Surveys,
Special issue: Position Statements on Strategic
Directions in Computing Research 28, 4es (Dec. 1996)
56. ACM, NY.
17. Wolper, P. The meaning of “formal”: From weak to
strong formal methods. STTT 1, 1–2 (1997), 6–8.
Mike hinchey ( email@example.com) is codirector of
Lero, the Irish Software Engineering Research Center,
and professor of software engineering at the University of
Michael Jackson ( firstname.lastname@example.org) is Visiting
Research Professor, Centre for Research in Computing,
The Open University, Milton Keynes, England.
Patrick Cousot ( Patrick.Cousot@ens.fr) is a professor of
computer science at the École Normale Supérieure. He is
a specialist in semantics, verification, and static analysis
of programs and complex systems and is the inventor of
Byron Cook ( email@example.com) is a researcher at
Microsoft’s Laboratory at Cambridge University, where
he has been working on the program termination prover
Terminator, the shape analysis engine SLAyer, and the
software model checker SLAM.
Jonathan P. Bowen ( firstname.lastname@example.org) is chairman
of Museophile Limited. He is contracted to work for Praxis
High Integrity Systems, applying formal methods for
software testing. He is also a visiting professor at King’s
College London and an emeritus professor at London
South Bank University.
Tiziana Margaria ( email@example.com) is chair
of service and software engineering at the Institute of
Informatics, Universität Potsdam, Germany. She is also
president of the European Association of Software Science
and Technology (EASS T).