practice
Doi: 10.1145/1378727.1378742
The answer to software reliability
concerns may lie in formal methods.
BY miKe hinche Y, michael JacKson, PatRicK cousot,
BYRon cooK, Jonathan P. Bo Wen, anD tiziana maRGaRia
software
engineering
and formal
methods
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
