conclusion

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 methods¹⁷ 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 environment.

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. ¹⁶ 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 attention here.

This quest continues…

 

References

1. Bowen, J.P. and Hinchey, M.G. Seven more myths of formal methods. IEEE Software 12, 4 (July 1995), 34–41.

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.

14. http://research.microsoft.com/SLAyer

15. http://research.microsoft.com/terminator

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. Springer Verlag.

 

Mike hinchey ( [e-mail]) is codirector of Lero, the Irish Software Engineering Research Center, and professor of software engineering at the University of Limerick, Ireland.

Michael Jackson ( [e-mail]) is Visiting Research Professor, Centre for Research in Computing, The Open University, Milton Keynes, England.

Patrick Cousot ( [e-mail]) 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 abstract interpretation.

Byron Cook ( [e-mail]) 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 ( [e-mail]) 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 ( [e-mail]) 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).