Process expansion: Action Refinement in the Large (PEARL)

The project concerns the top-down development of information systems. One convincing way to understand the complex systems that confront us daily in Computer Science is to specify their behaviors, abstracting implementation detail. But usually it is the implementations themselves that are of interest; for instance we may have just a specification and wish to find an implementation; or we may wish to understand, in greater detail than its specification, an existing implementation. By adopting the standard approach of Science, the top-down incremental method posits a series of designs, starting with the specification and ending with the implementation and having the property that each design conforms to its successor in the series.

More specifically we concentrate on distributed systems and topics broadly in:

1. developing ‘grain-less’ semantic theories for concurrent systems, where coarse-grained actions can be refined into (subsystems of) fine-grained actions (or conversely);

2. exploiting the freedom of moving across levels of abstraction (i.e. grain size) to develop scalable model-checking techniques and law-based incremental development methods;

3. application of the theories, techniques and methods to the verification and development of case studies including but not limited to concurrent non-blocking algorithms, multithreaded Java programs (with a weak-ordering memory model) and web-based transaction systems.

Funding: 225K USD from 2008 to 2001 by FDTC

Project members:

Ming Li, Weisong Li, Chris Ma, Jeff Sanders (PI), Xu Wang (CI), Qiwen Xu (CI) and Shaofa Yang