The Concurrency Factory- Practical Tools for the Design and Verification of Concurrent Systems

点击翻译按钮获取中文摘要

The goal of this project is to build an efficient, comprehensive and usable environment for design, verification, and implementation of concurrent systems. The system, which will cater to protocol engineers and software developers, will support process algebra as its underlying formalism and have the following features: o A graphical user interface that will allow the non-expert to design and simulate concurrent systems using process algebra. o A suite of design and analysis algorithms for concurrent systems; care will be taken to ensure that implementations of these algorithms will be efficient enough to be used on real-life systems. o A graphical compiler that will transform the graphic designs produced on the system into Ada or Occam programs. This will relieve the user of the burden of manually recoding their designs in the target language of their final system. o A uniform intermediate representation that will serve as the input format for all the tools in the system. Basing the representation on a widely recognized format, such as BLIF-MV or KISS2, will promote the exchange of tools with industrial and academic institutions. The system, the Concurrency Factory, will be written in C++ and execute under X-Windows so that it will be efficient, easily extendible, and highly portable. Moreover, all objects manipulated by the system will be stored in an object-oriented database, for efficient and uniform access. Realization of the Factory will require research in numerous areas including efficient algorithms for design and verification, with particular emphasis on techniques for state-space management and compositional analysis; computation of diagnostic information and its graphical presentation; and methods for compiling graphical descriptions of process algebra expressions into languages such as Ada and Occam.