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

这个项目的目标是为并发系统的设计、验证和实现构建一个高效、全面和可用的环境。该系统将满足协议工程师和软件开发人员的需求，将支持过程代数作为其底层形式，并具有以下特性：o图形用户界面，允许非专业人员使用进程代数设计和模拟并发系统。o一套并行系统的设计和分析算法；我们将小心翼翼地确保这些算法的实现足够有效，可以在实际系统中使用。o一种图形编译器，可将系统上产生的图形设计转换成Ada或Occam程序。这将减轻用户用最终系统的目标语言手动重新编写设计的负担。o统一的中间表示形式，作为系统中所有工具的输入格式。基于广泛认可的格式，如blifl - mv或KISS2，将促进与工业和学术机构的工具交流。该系统，即并发工厂，将用c++编写并在X-Windows下执行，因此它将是高效的、易于扩展的和高度可移植的。此外，系统操作的所有对象都将存储在面向对象的数据库中，以实现高效和统一的访问。工厂的实现需要在许多领域进行研究，包括设计和验证的有效算法，特别强调状态空间管理和成分分析的技术；诊断信息的计算及其图形化表示以及将过程代数表达式的图形描述汇编成诸如Ada和Occam的语言的方法。

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.