CAREER: Next Generation Model Checking

职业：下一代模型检查

• 批准号: 0448178
• 负责人: Mahesh Viswanathan
• 金额: $ 40万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-05-15 至 2011-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0448178&HistoricalAwards=false
• 关键词: CAREER; Next; Generation; Model; Checking

0448178 Mahesh Viswanathan U of Illinois @ UrbanaTITLE: CAREER: Next Generation Model Checking This research addresses the need to increase the reliability of software by continual analysis. One important approach to ensuring system correctness is model checking, in which the verification task is largely automatic and requires minimal user input. Though model checking has been successfully applied in practice, there are a couple of challenges that have limited its applicability. First, the representation of the system that the model checker analyzes is typically very large for most practical systems; this is often called the state space explosion problem. The second is that model checkers analyze a formal model of system which is often unavailable or difficult to construct. In this project, the PI plans to address these challenges by integrating ideas from computational learning theory and randomized algorithms to develop model checking algorithms with provably formal guarantees that can analyze black box systems within available computational resources.

0448178伊利诺伊州的Mahesh Viswanathan U @ Urbanatitle：职业：下一代模型检查此研究解决了通过持续分析提高软件可靠性的必要性。确保系统正确性的一种重要方法是模型检查，其中验证任务在很大程度上是自动的，并且需要最少的用户输入。尽管模型检查已成功地用于实践中，但仍有一些挑战限制了其适用性。首先，对于大多数实用系统，模型检查器分析的系统的表示通常非常大。这通常称为状态空间爆炸问题。第二个是模型检查员分析通常无法构建或难以构建的系统模型。 在该项目中，PI计划通过整合计算学习理论和随机算法的想法来解决这些挑战，以开发模型检查算法，并证明可以正式保证可以在可用的计算资源中分析黑匣子系统。