Verification Framework and Tools for Highly Reliable Cyber-Physical Systems

当今的网络物理系统(CPS)正变得越来越复杂，因为系统的行为和物理元素之间的紧密结合和协调。这种系统的例子可以在航空航天、航空电子系统、汽车等领域找到。验证和确认这些系统是一个耗时的过程，给计划时间表和预算带来了很高的风险。在设计这类系统的众多挑战中，我们在这里考虑的一个重要问题是，每个组件建模的不同方式以及它们彼此交互的方式。CPS系统的另一个重要方面与安全评估和可靠性分析有关。事实上，文献中已经表明，安全评估活动不同于使用正式方法的传统验证活动。使用正式的安全评估方法还远远不能对复杂的安全关键系统进行自动化验证。我们在这个研究项目中的目标是研究一个实用和正式的框架，该框架能够在建模为SysML行为图的组合的系统上进行安全风险评估和安全需求验证。系统建模语言(SysML)是一种OMG/INCOSE标准，它在现代系统和软件工程中发挥着核心作用。使用SysML作为建模语言，研究了形式化技术在关键系统安全评估中的应用。我们计划用SysML来表达这些安全需求，然后我们研究将这些结构、安全图和被测图以一种正式而优雅的方式结合起来的可能性。选择的安全场景和具有实例化的安全属性的组合图之间的交互作用的结果被用于通过应用概率验证来量化安全风险。为了处理验证过程的可扩展性，将对概率系统的组成验证和抽象等技术进行研究。最后，为了显示我们方法的有效性，我们将调查我们的方法在几个基准上的使用情况。我们的目标应用将从航空电子系统和航空航天应用中选择。

Today's Cyber-Physical Systems (CPS) are becoming more and more complex because of the tight combination, and the coordination between, the system's behavior and physical elements. Examples of such system can be found in aerospace, avionics systems, automotive, ... etc. Verifying and validating those systems is a time consuming process that puts high risk on program schedule and budget. Among the many challenges in designing such system, one important problem that we consider here, arises from the different ways in modeling each component and the way they interact with each other. Another important aspect of CPS systems is related to safety assessment and reliability analysis. In fact, it has been shown in the literature that safety assessment activities are different from the traditional verification activities where formal methods are used. The use of Formal Methods for safety assessment is still far from an automated verification of complex safety critical systems. Our goal in this research program is to investigate a practical and formal framework that enables safety risk assessment and safety requirements verification on a system modeled as a composition of SysML behavioral diagrams. The System Modeling Language (SysML) is an OMG/INCOSE standard that plays a central role in modern systems as well as in software engineering. Using SysML as a modeling language, we investigate the use of formal techniques for the safety assessment of critical systems. We plan to express those safety requirements in SysML, and then we study the possibility of combining these structures, safety diagrams and the diagram under test in a formal and an elegant way. The result of the interaction between selected safety scenarios and the composed diagrams with the instantiated safety properties are used to quantify safety risk by applying probabilistic verification. To handle the verification process scalability, techniques such compositional verification and abstraction will be investigated for probabilistic systems. Finally, to show the effectiveness of our approach, we will investigate the use of our methodology on several benchmarks. Our target applications will be chosen from avionics systems and aerospace applications.