CAREER: Robustness Analysis of Uncertain Programs: Theory, Algorithms, and Tools

职业：不确定程序的鲁棒性分析：理论、算法和工具

• 批准号: 0953507
• 负责人: Swarat Chaudhuri
• 金额: $ 42.65万
• 依托单位: Pennsylvania State Univ University Park
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-05-01 至 2012-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0953507&HistoricalAwards=false
• 关键词: CAREER; Robustness; Analysis; Uncertain; Programs

This research program will develop mathematical techniques to automatically prove the robustness of computer programs operating under uncertainty. The aim is to bridge the gap between control-theoretic studies of robustness, on the one hand, and program semantics and analysis on the other. In cyberphysical systems, where sensor-derived data from the physical world is intertwined with computations, uncertainty arises from volatile or erroneous sensor data. Such systems demand predictable responses to perturbations of the system's initial conditions, otherwise they will be unreliable. The project has three themes: (1) Theory: It will create comprehensive semantics of robustness properties such as continuity and stability in the setting of imperative programs over complex data types. (2) Algorithms: Analysis algorithms are needed to prove robustness of programs, or alternately find violations of robustness. Scalable, lightweight analyses will be developed along with precise but heavyweight methods. (3) Tools: These analyses will be implemented in tools applicable to software for real-world cyber-physical systems.

该研究计划将开发数学技术，以自动证明在不确定性下运行的计算机程序的鲁棒性。目的是弥合鲁棒性的控制理论研究，另一方面是程序语义和另一方面的分析。在网络物理系统中，来自物理世界的传感器衍生数据与计算交织在一起，不确定性来自挥发性或错误的传感器数据。这样的系统需要对系统初始条件的扰动的可预测响应，否则它们将不可靠。 该项目具有三个主题：（1）理论：它将创建稳健性属性的综合语义，例如连续性和稳定性，以在复杂数据类型的命令式程序中。 （2）算法：需要分析算法来证明程序的鲁棒性，或者选择违反鲁棒性。可扩展，轻质分析将以精确但重量级的方法进行开发。 （3）工具：这些分析将用于适用于现实世界网络物理系统软件的工具。