Verification Framework and Tools for Highly Reliable Cyber-Physical Systems

点击翻译按钮获取中文摘要

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.