Design and Verification Methodologies

There are two important observations about the current state in design and verification of concurrent systems:

• There are many proposed techniques, and guidelines for using these techniques, that differ in quality and applicability (see also Sections 2.2 and 3.2).
• The design and also the verification of many concurrent systems happen to be similar exercises.

The transformation of the existing array of design and verification techniques into sound and tested methodologies, is one of the major challenges facing the concurrency community in the next decade. Moreover, the resulting methodologies should extend the range of existing techniques to applications orders of magnitude larger in size and complexity.

Similar to concerns raised in Section 3.2 regarding a uniform semantic framework for concurrency, we should also seek ways to combine methodologies, to better suit the demands of a given application, and, relatedly, develop an application-oriented taxonomy of methodologies.

To produce a next generation of truly usable methodologies, the following issues must be addressed:

Algorithmic support.

Further advances (i.e., beyond those listed in Section 2.2.2) are needed to better cope with the state-space explosion problem inherent to concurrent system design and verification. Compositional methods, in which the analysis of a system is decomposed into an analysis of its components, and refinement methods, in which a system is analyzed at varying levels of abstraction, may play a key role here (see also Section 3.2).

Tool support.

The problems confronting today's tools such as bugs and lack of portability and scalability, need to be addressed. Furthermore, tools should be better integrated into the software engineering lifecycle. Traditionally, software engineering devotes much attention to organizational and procedural issues in software development and relatively little to methods for system analysis; in this respect, it resembles a management discipline rather than an engineering one. Tools based on concurrency theory offer a particularly appropriate starting point for putting the engineering back into software engineering.