Verification of Open-Loop Embedded Control Systems

开环嵌入式控制系统的验证

• 批准号: 0820072
• 负责人: W. Rance Cleaveland
• 金额: $ 35万
• 依托单位: University of Maryland, College Park
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-08-01 至 2012-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0820072&HistoricalAwards=false
• 关键词: Verification; Open; Loop; Embedded; Control

NSF Proposal 0820072Title: Verification of Open-Loop Embedded Control SystemsPI: Rance CleavelandThis project develops automated techniques for efficiently analyzing the correctness of open-loop embedded control software. Such software is widespread in the real-world, in automotive, flight-control, medical-device and other human-in-the-loop applications, where environmental behavior is unpredictable. The research effort is based on the observation that such software can be effectively modeled using a particular mathematical formalism called timed automata. The specific topics being studied include: 1) Model checking: novel on-the-fly algorithms, in which system behavior is explored in a demand-driven manner, are being developed for checking properties of timed automata. 2) Industry-standard modeling and model checking: strategies are being devised for adapting the model-checking tools to industry-standard modeling notations such as Simulink© and for exploiting model structure to enable verification of large models that arise in practice. The significance and impact of the work derive from the more thorough verification of control software the new technologies will enable. By automating formal validation activities and supporting widely used modeling tools, the research will empower engineers to conduct more intensive analyses of their control-system designs earlier in the life-cycle than current techniques allow.

NSF 提案 0820072 标题：开环嵌入式控制系统的验证 PI：Rance Cleaveland 该项目开发自动化技术，用于有效分析开环嵌入式控制软件的正确性。此类软件在现实世界中广泛使用，例如汽车、飞行控制、医疗设备和其他人机交互应用，这些领域的环境行为是不可预测的。 研究工作基于这样的观察：可以使用称为定时自动机的特定数学形式对此类软件进行有效建模。 正在研究的具体主题包括： 1）模型检查：正在开发新颖的即时算法，以需求驱动的方式探索系统行为，用于检查定时自动机的属性。 2) 行业标准建模和模型检查：正在制定策略，使模型检查工具适应行业标准建模符号（例如 Simulink©），并利用模型结构来验证实践中出现的大型模型。这项工作的意义和影响源于新技术将实现的对控制软件的更彻底的验证。 通过自动化正式验证活动并支持广泛使用的建模工具，该研究将使工程师能够比当前技术允许的更早地在生命周期中对其控制系统设计进行更深入的分析。