CPS: Small: Collaborative Research: Methods and Tools for the Verification of Cyber-Physical Systems

CPS：小型：协作研究：网络物理系统验证的方法和工具

• 批准号: 0930510
• 负责人: Hao Zheng
• 金额: $ 26万
• 依托单位: University of South Florida
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-15 至 2013-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0930510&HistoricalAwards=false
• 关键词: CPS; Small; Collaborative; Research; Methods

CPS:Small:Collaborative Research: Methods and Tools for the Verification of Cyber-Physical SystemsThe objective of this research is to investigate and develop methods and tools for the analysis and verification of cyber-physical systems. The approach is to augment the methods and tools that have been developed at the University of Utah and the University of South Florida for modeling and verification of asynchronous and analog/mixed-signal circuits to address challenges in cyber-physical system verification.This research will develop a unified framework with methods and tools which include an integrated formalism to comprehensively model discrete/continuous, functional/timing, synchronous/asynchronous, and deterministic/stochastic behavior. These tools will also include algorithms to analyze behavior and verify that it satisfies the correctness requirements on functionality, timing, and robustness. Finally, they will include abstraction and compositional reasoning approaches to enable large systems to be analyzed and verified efficiently.Since cyber-physical systems are becoming ubiquitous, improvements in such systems such as higher reliability, better fault-tolerance, improved performance, and lower design costs will have tremendous positive impact on society. Results from this research will be transferred to the cyber-physical systems community and other application domains by both publishing papers in related conferences and journals as well as by freely distributing tools via the Internet. Both graduate and undergraduate students will be engaged in this multi-institutional research where they will be exposed to the latest research in formal and probabilistic analysis. Early involvement of undergraduate students may help encourage them to attend graduate school. This research project will also recruit underrepresented and female students to allow it to reach broader audiences.

CPS：小型：协作研究：信息物理系统验证的方法和工具本研究的目的是研究和开发信息物理系统分析和验证的方法和工具。 该方法是为了增强犹他州大学和南佛罗里达大学为异步和模拟/混合信号电路的建模和验证而开发的方法和工具，以解决信息物理系统验证中的挑战。本研究将开发一个统一的框架，其中包括一个综合的形式主义，全面建模离散/连续，功能/时序，同步/异步，和确定性/随机性行为。 这些工具还将包括分析行为的算法，并验证它是否满足功能，时序和鲁棒性的正确性要求。 最后，它们将包括抽象和组合推理方法，使大型系统能够被有效地分析和验证。由于网络物理系统变得无处不在，这些系统的改进，如更高的可靠性，更好的容错性，提高性能，降低设计成本将对社会产生巨大的积极影响。 这项研究的结果将通过在相关会议和期刊上发表论文以及通过互联网免费分发工具转移到网络物理系统社区和其他应用领域。 研究生和本科生都将参与这种多机构的研究，他们将接触到正式和概率分析的最新研究。 本科生的早期参与可能有助于鼓励他们进入研究生院。 这一研究项目还将招募代表性不足的学生和女学生，使其能够接触到更广泛的受众。