Model-based Approach for System-Level Testing and Validation

Iowa State University, Ames IA

Investigators

Abstract

Modern distributed Cyber-Physical Systems (CPS) such as avionics, automotive, power systems, nuclear reactors, medical devices are safety-critical, requiring high-degree of dependability and must be carefully tested, validated, and verified for correctness, safety, security, performance and fault-tolerance. The project proposes a unified model-based framework offering innovations in modeling, test generation and validation, error-localization and compositional verification methods. The importance of model-based approaches to correctness and robustness of distributed CPS designs is well recognized by industry, and several efforts are underway in academia and industry. The project will make additional contributions by identifying and filling some of the gaps/limits of the current state-of-art. The translation from heterogeneous behavioral models of distributed CPS components to common unified automata based models shall find its use in other formal reasoning (e.g., monitoring, model-checking, synthesis, security analysis). The research outcomes, including supporting software, will be made available through PI's homepage and publications. The PI has been developing Model-based approaches for Cyber-Physical Systems--both design-time (testing and validation) and run-time (monitoring, diagnosis and control), including testing approach for reactive software developed using Simulink/Stateflow, and fault-tolerance approach for such reactive software. For system-wide testing and validation, a system-level modeling language (AADL or SysML) can formally capture the end-to-end CPS architecture, component behaviors, requirements, and failure-modes. Also, modeling and analysis tools, including code-generators and model-checkers, exist. Our contribution will be to provide new additions on unified system-level modeling, testing and verification for distributed CPS, supporting new features: (i) Novel approaches for CPS components modeling capturing implementation imperfections, process randomness, timing and concurrency features; (ii) Approach to interface and adjoin component models to obtain an overall model for system-level analysis; (iii) Model-based system-level testing approach for stochastic dynamical systems introducing probabilistic guarantees of coverage, and error-localization; (iv) Quantifier elimination based compositional property verification; (v) Scalable approaches to reachability analysis in hybrid systems. Specifically, these would be enabled through (i) A modeling approach for software under hardware constraints of computing precision and delays to enable an early and cost-efficient processor-in-the-loop testing/verification; (ii) For system-level testing/verification, a unified components-based concurrent system modeling in form of communicating Input-Output Stochastic Hybrid Automata, capable of capturing timing issues (delays, drifts, multi-rate processing), randomness of physical components, and concurrency; (iii) Model-based probabilistic approach for system-level testing, validation and error localization, accounting for uncertainties. (iv) Compositional verification approach in a component-based design paradigm by employing quantifier elimination; (v) Novel scalable approaches to reachability analysis in hybrid and real-time systems using iterative face-lifting and partitioning, and for real-time systems using mixed integer linear programming based bounded model-checking.