Doi: 10.1145/1378727.1378742
THE SOFTWARE ENGINEERING community has devised many techniques, tools, and approaches aimed at improving software reliability and dependability. These have had varying degrees of success, some with better results in particular domains than others, or in particular classes of applications. A popular, although not uncontroversial, approach is known as formal methods, whereby a specification notation with formal semantics, along with a deductive apparatus for reasoning, is used to specify, design, analyze, and ultimately implement a hardware or software (or hybrid) system.
Such an approach is often thought to be difficult to apply and to require significant mathematical experience. 1, 11 Experience has demonstrated that developers without significant mathematical ability can at least understand and use formal specifications,
even if greater mathematical ability and specialization in various areas of mathematics and engineering are needed for more challenging formal methods-related activities such as verification and refinement, and even the task of writing formal specifications themselves. As automated formal methods slowly become a natural part of the design process, we also experience higher dependability levels as a standard trait of software products.
A key issue, however, is the need for those applying formal methods to be able to abstract and to model systems at an appropriate level of representation— that is, to develop solid design principles and apply them to software development. This is particularly true when proving properties of more complex systems involving significant concurrency and interaction among components. When we wish to prove properties, it is often easier—and necessary—to prove them at a more abstract level, exploiting the idea of abstract interpretation.
This article contains contributions from three world-renowned experts in the fields of software engineering, abstract interpretation, and verification of concurrent systems: Michael A. Jackson, Patrick Cousot, and Byron Cook. Their contributions are based on their keynote speeches at the IEEE’s Fifth International Conference on Software Engineering and Formal Methods, held in London, Sept. 10–14, 2007. The aim of the conference series is to bring together practitioners and researchers in the fields of formal methods and software engineering with the goal of exploiting synergies and furthering our understanding of specialization, abstraction, and verification techniques, among other areas.
Declining Dependability levels Computer-based systems are pervasive and now influence almost every facet of our lives. They wake us in the morning, control the cooking of our food, entertain us in the guise of media players, help in avoiding traffic congestion, control or identify (via GPS navigation
References:
Archives