Practical Formal Methods for the Design and Analysis of Complex Concurrent Systems

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

9804665 This project will develop a new programming and specification language for distributed systems, IOA, with explicit support for parallel composition and levels of abstraction. It will also develop computer tools to manipulate programs and descriptions written in the IOA language; such tools will include a simulator, interfaces to existing theorem-provers and model-checkers, and a real code-generator. The language and all the tools will rest firmly upon a previously-developed mathematical foundation consisting of input/output automata. They will enable the production of running systems that are provably correct, relative to assumptions about externally-provided system services. These tools will be built and tested using examples chosen from the area of high-performance, fault-tolerant distributed systems, with particular emphasis on group communication services and distributed shared memory services."***