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.