Specification Formalism for Component-Based Concurrent Systems

9804091本项目的重点是为面向组件的或开放的并发系统开发有效的规范形式化。讨论的具体主题包括：调查开放系统的隐含规范；开发有效但通用的时态逻辑模型检查技术，包括开放系统的模型检查技术。隐式规范采用上下文的形式，或带有“洞”的系统描述，正在开发的组件将被插入其中。这种规范的动机是实用的：它们可以使用给出系统描述的相同符号来编写，而不需要用户学习额外的逻辑符号。本项目调查此类规范的表达能力，并进行案例研究。模型检查器允许自动确定系统何时享有时态逻辑中的属性。该项目这一部分的结果将显示如何给出适用于所有时态逻辑的通用而有效的模型检查程序；这将改善现有的技术状态，即每一个新逻辑都需要新的程序。作为一个整体，该项目将产生结果，从而改进自动化方法，从而改进用于说明和推理面向组件的并发软件的分析工具。*

9804091 This project focuses on the development of effective specification formalisms for component-oriented, or open, concurrent systems. The specific topics addressed include: the investigation of implicit specifications for open systems; and the development of efficient yet generic model-checking techniques for temporal logics, including those for open systems. Implicit specifications take form of contexts, or system descriptions with "holes," into which the component being developed is to be inserted. The motivation for such specifications is practical: they may be written using the same notation in which the system description is given and do not require users to learn additional logical notations. This project investigates the expressiveness of, and case studies involving, such specifications. Model checkers permit the automatic determination of when systems enjoy properties in temporal logics. The results of this part of the project will show how generic yet efficient model-checking procedures that work for all temporal logics may be given; this will improve on the existing state of the art, which requires new procedures for each new logic. The project as a whole will yield results leading to improved automated methodologies, and hence better analysis tools, for specifying and reasoning about component- oriented concurrent software.***