Research Directions for Concurrency

Joseph Sifakis
Laboratoire VERIMAG,
Joseph.Sifakis@imag.fr

The main achievements of research on concurrency concern the development of languages, models and underlying verification theories.
Executable specification languages include asynchronous ones like CSP and synchronous languages like Esterel, Lustre and the Statecharts. The work on process calculi contributed a lot to understand the problem of compositionality and led to investigation of theories for fully abstract semantics.

The study of logical specification languages such as the various temporal logics and mu-calculi, allowed understanding what are significant classes of properties of concurrent systems. Interesting results enable combining logical and executable specifications.

For both logical and executable specifications, verification methods and tools have been developed either by using proof methods or by algorithmic methods.

In the nineties, research on timed and hybrid systems becomes very active. Different timed extensions of existing formalisms with quantitative time are studied: timed automata, timed process algebras, real-time temporal logics. As in the untimed case, the inter-relations between these formalisms are also extensively explored. Finally, specific verification methods have been developed.

Concurrency theories have currently a limited impact on specification languages and design methodologies used in practice. Of course, ideas about communicating sequential processes influenced the design of languages like ADA or Lotos. The ideas on reactive synchronous systems are at the basis of synchronous languages. However, system designers widely use semi-formal languages with obvious limitations. An important question is whether and how the developed results can help overcoming these limitations. Results on verification by model checking or theorem proving find applications in many areas such as hardware, protocols and critical real-time systems. However, the verification methods do not make use of deep results of concurrency theory (they are based on flattening and forget most information about structure). In the future, it is important to continue developing verification methods and tools adapted to existing languages and integrated in development environments with other validation methods like testing and simulation.

We believe that future research should focus on the study of domain specific specification languages, their semantics and their efficient implementation techniques. The relationship between synchrony and asynchrony is not still well understood, one of the main problems being the introduction of notions of time to asynchronous languages. We distinguish two important research directions: