Visible to the public Verification and Validation of a Cyber-Physical System in the Automotive Domain

TitleVerification and Validation of a Cyber-Physical System in the Automotive Domain
Publication TypeConference Paper
Year of Publication2017
AuthorsKang, E. Y., Mu, D., Huang, L., Lan, Q.
Conference Name2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C)
Date Publishedjul
KeywordsAnalytical 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
AbstractSoftware 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.
Citation Keykang_verification_2017