Verification Framework and Tools for Highly Reliable Cyber-Physical Systems

高可靠网络物理系统的验证框架和工具

• 批准号: 261438-2013
• 负责人: AitMohamed, Otmane
• 金额: $ 1.46万
• 依托单位: Concordia University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=571041
• 关键词: Verification; Framework; Tools; Highly; Reliable

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.

由于系统的行为和物理元素之间的紧密组合以及协调性，当今的网络物理系统（CPS）变得越来越复杂。该系统的示例可以在航空航天，航空电子系统，汽车，...等。验证和验证这些系统是一个耗时的过程，它在计划时间表和预算上造成了高风险。 在设计此类系统的许多挑战中，我们在这里考虑的一个重要问题是源于对每个组件建模及其相互作用方式的不同方式。 CPS系统的另一个重要方面与安全评估和可靠性分析有关。实际上，在文献中已经表明，安全评估活动与使用正式方法的传统验证活动不同。使用正式方法进行安全评估远非对复杂安全关键系统的自动验证。我们在本研究计划中的目标是研究一个实用和正式的框架，该框架能够对以SYSML行为图组成的系统进行安全风险评估和安全要求验证。系统建模语言（SYSML）是OMG/INCOSE标准，在现代系统和软件工程中都起着核心作用。 使用SYSML作为建模语言，我们研究了对关键系统的安全评估的正式技术的使用。 我们计划在SYSML中表达这些安全要求，然后研究以正式和优雅的方式结合这些结构，安全图和正在测试的图表的可能性。选定的安全方案与与实例化安全性能的组合图之间相互作用的结果用于通过应用概率验证来量化安全风险。为了处理验证过程可伸缩性，将研究概率系统的组成验证和抽象。最后，为了展示我们的方法的有效性，我们将研究我们的方法在几个基准上的使用。我们的目标应用将从航空电子系统和航空航天应用中选择。