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

“该奖项是根据2009年美国复苏和再投资法案(公法111-5)资助的。”摘要：复杂系统的正式分析--一项涉及CMU、CUNY、NYU、Stony Brook、UMD、Cornell、JPL的合作提案。该考察队在负责人Pi Edmund M.Clarke的领导下，将开发新的计算工具，帮助科学家和工程师分析和理解他们为从系统生物学到嵌入式控制等应用领域开发的复杂模型的行为。基于模型检测和抽象解释(MCAI)这两种成熟的自动验证数字电路设计和嵌入式软件性能的方法的成功，本研究项目将把MCAI范式扩展到具有复杂的连续动力学和概率行为的系统。为研究提供技术驱动因素和试验台的挑战问题包括：了解胰腺癌的前兆和病程；预测心房颤动的发生；以及对汽车和航空航天控制系统的行为获得深入的设计时洞察。最终，这次探险预计将提供重要的工具，使医疗保健研究人员能够发现更好的疾病治疗方法，并使工程师能够建造更安全的飞机和其他复杂的系统。为这次探险聚集的世界级科学家和工程师团队包括两名图灵奖获得者、一名国家科学奖章获得者和其他著名研究奖项的获得者。外展活动包括开发一个名为复杂系统科学工程的新的、雄心勃勃的、高度跨学科的教育计划，每年为本科生举办一个以少数族裔为重点的间歇研讨会，让他们了解和分析复杂的嵌入式和生物系统，并将在纽约州立大学的成员机构雷曼学院主办；为本科生研究提供大量资金支持；学生参与美国国家航空航天局喷气推进实验室研究分支机构计划；以及为本科生、研究生和博士后培训人员提供其他研究机会。更多信息：http://www.mcai2.org/

"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/