Position Statement for Formal Methods and Concurrency
Rajeev Alur, Bell Labs
Case studies in recent years have demonstrated that formal methods
can indeed play a role in the design of complex distributed systems.
While the interest is more evident in the hardware industry, there is
also a growing awareness among software designers of the potential of
formal methods to enhance the current software engineering tools.
Consequently, the future of formal methods in general, and verification
and concurrency theory in particular, looks brighter, and we should make
full use of this opportunity to influence the practice. I have summarized
my thoughts along four directions below.
Writing rigorous models and specifications is tedious, but once such
mathematical descriptions are available, our tools should perform powerful
analysis that provides useful feedback. This analysis may be partial,
but should be as automated as possible. Indeed, the role of formal methods
is to provide rapid prototyping and sophisticated debugging rather than
design of provably correct systems. Examples of such analyses include
checking consistency, type checking, and model checking.
Formal methods can be introduced in the design cycle at various phases:
for requirements, for code development, for testing. For each phase, there
are various concerns (such as reliability, security) and numerous formalisms.
Even for the well-defined problem of model checking for finite-state machines,
some tools are well-suited for asynchronous protocols, while some others for
synchronous hardware. A challenging problem is offer the designer a consistent
and simple view, and a common platform that can effectively manipulate formal
specifications at different levels. Such an integration would require
collaborative research among different subdisciplines within our community.
For effective use of formal methods, designers need to feel comfortable
with formal reasoning. Structured programming has found its way into most
computer science curricula, but not logic and formal methods. These topics
need to be taught as tools that are universally applicable in computer
science. A first obstacle to this goal is the perception among our colleagues
in other fields of computer science; formal methods is yet to be recognized
as an essential discipline.
This subject has a variety of foundational problems for research, ranging
from issues in semantics and concurrency theory to algorithmic challenges
for coping with the computational complexity of model checking. Recent
developments in hybrid systems have led to interdisciplinary research with
control theory. It is this exciting range of problems that keeps the
area vibrant and attracts young researchers, we should continue our support
for such research.