| Title | Verification and Validation of a Cyber-Physical System in the Automotive Domain |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Kang, E. Y., Mu, D., Huang, L., Lan, Q. |
| Conference Name | 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C) |
| Date Published | jul |
| Keywords | Analytical models, Automotive engineering, autonomous traffic sign recognition vehicle, Cameras, CPS, cyber-physical system validation, cyber-physical system verification, Cyber-physical systems, delays, domain specific architectural language, EAST-ADL, EAST-ADL constraints, EAST-ADL/Stateflow, Embedded systems, energy constraints, extended ERT constraints, formal statistical analysis, formal verification, functional quality assurance, mapping rules, modified EAST-ADL, nonfunctional quality assurance, parallel languages, power aware computing, probabilistic extension, probability, probability parameters, pubcrawl, quality assurance, resilience, Resiliency, S/S models, safety-critical automotive embedded system design, Scalability, security, semantics denotation, Simulink Design Verifier, Simulink/Stateflow integration, Software development, software packages, software quality, Stochastic computing, Stochastic Computing Security, Stochastic processes, traffic engineering computing, transformed energy-aware real-time behaviors, UPPAAL models, UPPAAL-SMC, verifiable UPPAAL- SMC models, Verification & Validation, Wheels |
| Abstract | Software development for Cyber-Physical Systems (CPS), e.g., autonomous vehicles, requires both functional and non-functional quality assurance to guarantee that the CPS operates safely and effectively. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time (ERT) behaviors modeled in EAST-ADL/Stateflow into UPPAAL models amenable to formal verification. Previous work is extended in this paper by including support for Simulink and an integration of Simulink/Stateflow (S/S) within the same too lchain. S/S models are transformed, based on the extended ERT constraints with probability parameters, into verifiable UPPAAL-SMC models and integrate the translation with formal statistical analysis techniques: Probabilistic extension of EAST-ADL constraints is defined as a semantics denotation. A set of mapping rules is proposed to facilitate the guarantee of translation. Formal analysis on both functional- and non-functional properties is performed using Simulink Design Verifier and UPPAAL-SMC. Our approach is demonstrated on the autonomous traffic sign recognition vehicle case study. |
| DOI | 10.1109/QRS-C.2017.62 |
| Citation Key | kang_verification_2017 |
Verification and Validation of a Cyber-Physical System in the Automotive Domain