Specification Formalism for Component-Based Concurrent Systems

基于组件的并发系统的规范形式

• 批准号: 9804091
• 负责人: W. Rance Cleaveland
• 金额: $ 14.8万
• 依托单位: North Carolina State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-07-01 至 1998-12-15
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9804091&HistoricalAwards=false
• 关键词: Specification; Formalism; Component; Based; Concurrent

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.***

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