Verification Framework and Tools for Highly Reliable Cyber-Physical Systems

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

• 批准号: 261438-2013
• 负责人: AitMohamed, Otmane
• 金额: $ 1.46万
• 依托单位: Concordia University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2017
• 资助国家: 加拿大
• 起止时间: 2017-01-01 至 2018-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=634391
• 关键词: 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 表达这些安全要求，然后研究以正式且优雅的方式将这些结构、安全图和被测图结合起来的可能性。所选安全场景与具有实例化安全属性的组合图之间的交互结果用于通过应用概率验证来量化安全风险。为了处理验证过程的可扩展性，将针对概率系统研究组合验证和抽象等技术。最后，为了展示我们方法的有效性，我们将研究我们的方法在几个基准上的使用情况。我们的目标应用将从航空电子系统和航空航天应用中选择。