Collaborative Research: Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology

合作研究：以嵌入式控制和系统生物学为重点的下一代模型检查和摘要解释

• 批准号: 0926181
• 负责人: Edmund Clarke
• 金额: $ 384.57万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-01 至 2015-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0926181&HistoricalAwards=false
• 关键词: Collaborative; Research; Next; Generation; Model

"This award is funded under the American Recovery and Reinvestment Act of 2009(Public Law 111-5)."Summary: Formal Analysis of Complex SystemsA Collaborative Proposal Involving CMU, CUNY, NYU, Stony Brook, UMD, Cornell, JPLThis Expedition, under the directorship of Lead PI Edmund M. Clarke, will develop new computational tools to help scientists and engineers analyze and understand the behavior of the complex models they develop for application domains ranging from systems biology to embedded control. Building on the success of model checking and abstract interpretation (MCAI), two well-established methods for automatically verifying properties of digital circuit designs and embedded software, this research project will extend the MCAI paradigm to systems with complex continuous dynamics and probabilistic behaviors. Challenge problems providing technology drivers and testbeds for the research include: understanding the precursors and course of pancreatic cancer; predicting the onset of atrial fibrillation; and obtaining deep design-time insights into the behavior of automotive and aerospace control systems. Ultimately, this Expedition is expected to provide vital tools that will enable health-care researchers to discover better treatments for disease and will allow engineers to build safer aircraft and other complex systems.The world-class team of scientists and engineers assembled for this Expedition includes two Turing Award winners, a recipient of the National Medal of Science, and awardees of other prestigious research prizes. Outreach consists of the development of a new, highly ambitious and highly cross-discipline educational program called Complex Systems Science Engineering, an annual Minority-Focused Intersession Workshop for Undergraduates on Understanding and Analyzing Complex Embedded and Biological Systems to be hosted at member institution Lehman College, CUNY; substantial financial support for undergraduate research; student involvement in the NASA JPL Research Affiliates Program; and other research opportunities for undergraduate and graduate students and postdoctoral trainees.More information: http://www.mcai2.org/

“该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。“总结：复杂系统的形式化分析一项涉及CMU、CUNY、NYU、斯托尼布鲁克、UMD、Cornell、JPL的合作计划。克拉克将开发新的计算工具，以帮助科学家和工程师分析和理解他们为从系统生物学到嵌入式控制等应用领域开发的复杂模型的行为。 基于模型检测和抽象解释（MCAI）的成功，两个成熟的方法自动验证数字电路设计和嵌入式软件的属性，本研究项目将扩展MCAI范式的系统与复杂的连续动态和概率行为。为研究提供技术驱动和测试平台的挑战性问题包括：了解胰腺癌的前兆和病程;预测房颤的发作;以及对汽车和航空航天控制系统的行为进行深入的设计时洞察。最终，这次远征有望提供重要的工具，使医疗保健研究人员能够发现更好的疾病治疗方法，并使工程师能够建造更安全的飞机和其他复杂系统。这次远征的世界级科学家和工程师团队包括两名图灵奖获得者，一名国家科学奖章获得者，以及其他着名研究奖项的获得者。外展包括开发一个新的、雄心勃勃且高度跨学科的教育项目，称为复杂系统科学工程，这是一个针对本科生的年度以少数族裔为重点的闭会期间研讨会，旨在了解和分析复杂的嵌入式和生物系统，将在成员机构举办纽约市立大学雷曼学院;为本科生研究提供大量财政支持;学生参与NASA喷气推进实验室研究附属计划;和其他研究机会的本科生和研究生和博士后实习生。更多信息：http://www.mcai2.org/