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

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

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.