Methodologies for the Automatic Verification of Concurrent Systems

并发系统自动验证方法

• 批准号: 9402807
• 负责人: W. Rance Cleaveland
• 金额: $ 16.56万
• 依托单位: North Carolina State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1994
• 资助国家: 美国
• 起止时间: 1994-09-15 至 1998-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9402807&HistoricalAwards=false
• 关键词: Methodologies; Automatic; Verification; Concurrent; Systems

9402807 Cleaveland The goals of this project involve the development of practical approaches to the automatic verification of finite-state concurrent systems, including hardware designs, communications protocols, and software requirements specifications. Such systems are notoriously difficult to design, debug and maintain, owing to the subtle and often unanticipated interactions between components that parallelism induces. One appealing approach to overcoming these problems involves the use of mathematical reasoning to ensure that systems behave as intended; this research aims at making the use of such formal analysis practical by developing suitable techniques, and associated software tools, that enable designers to analyze their systems as they are building them. The proposed work would develop along the following lines: Research would undertaken into more efficient algorithms for determining the correctness of concurrent systems; techniques would investigated for enabling the analysis of larger systems than can currently be managed; he development of usable graphical and textual design languages would undertaken, and appropriate tools implemented; methods would develop and implement for reasoning about real-time systems and about the relative reliability of systems. ***

9402807 Cleaveland 该项目的目标涉及开发有限状态并发系统自动验证的实用方法，包括硬件设计、通信协议和软件需求规范。 由于并行性引起的组件之间微妙且经常无法预料的交互，此类系统的设计、调试和维护非常困难。 克服这些问题的一种有吸引力的方法是使用数学推理来确保系统按预期运行。这项研究的目的是通过开发合适的技术和相关的软件工具，使这种形式分析的使用变得实用，使设计人员能够在构建系统时对其进行分析。 拟议的工作将沿着以下方向发展： 研究更有效的算法来确定并发系统的正确性； 将研究能够分析比目前可管理的更大系统的技术；将开发可用的图形和文本设计语言，并实施适当的工具；将开发和实施用于推理实时系统和系统相对可靠性的方法。 ***