LMC: A System for the Specification and Evaluation of Logic-Based Model Checking

LMC：基于逻辑的模型检查的规范和评估系统

• 批准号: 9705998
• 负责人: Scott Smolka
• 金额: $ 122.37万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-08-15 至 2003-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9705998&HistoricalAwards=false
• 关键词: LMC; System; Specification; Evaluation; Logic

The objective of this project is to deploy the latest advances in concurrency research and in logic programming systems to build a software environment called LMC for system specification and verification. LMC's main function is model checking: determining whether a software system possesses a particular formally specified property. LMC is built from two independently developed systems, each of significant interest in its own domain: the Concurrency Factory verification toolkit (developed jointly by Stony Brook and NC State), and the XSB tabled logic programming system (developed by Stony Brook). The anticipated benefits of this research include the following: a model checker in XSB is specified at the level of semantic equations, meaning a system for a specific specification language and logic can be coded in several hundred lines of XSB code rather than in tens of thousands of lines of C++ code; the programmability of XSB allows for direct encoding of important model checking optimizations; in XSB it is possible to interleave arbitrarily model checking computational steps with deduction steps without penalizing the performance of the former. These features are expected to make LMC a practical tool for formally assuring the correctness of critical software systems such as network protocols.

这个项目的目标是部署并发研究和逻辑编程系统的最新进展，建立一个软件环境称为LMC的系统规范和验证。LMC的主要功能是模型检查：确定软件系统是否具有特定的形式化属性。LMC由两个独立开发的系统构建而成，每个系统都在自己的领域有着重要的意义：并发工厂验证工具包（由斯托尼布鲁克和NC State联合开发）和XSB表格逻辑编程系统（由斯托尼布鲁克开发）。 本研究的预期好处包括：XSB中的模型检查器是在语义方程级指定的，这意味着可以用几百行XSB代码而不是几万行C++代码来编码特定规范语言和逻辑的系统; XSB的可编程性允许直接编码重要的模型检查优化;在XSB中，可以任意地将模型检验计算步骤与演绎步骤交错，而不会损害前者的性能。这些功能有望使LMC成为一种实用的工具，用于正式确保关键软件系统（如网络协议）的正确性。