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.

1. AUTOMATION 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.
2. INTEGRATION 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.
3. EDUCATION 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.
4. FOUNDATIONS 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.