Model-based Approach for System-Level Testing and Validation

现代分布式网络物理系统（CPS），如航空电子设备、汽车、电力系统、核反应堆、医疗设备等，对安全至关重要，需要高度的可靠性，必须仔细测试、验证和验证其正确性、安全性、安全性、性能和容错性。该项目提出了一个统一的基于模型的框架，在建模、测试生成和验证、错误定位和成分验证方法方面提供了创新。基于模型的方法对于分布式CPS设计的正确性和健壮性的重要性已得到业界的广泛认可，学术界和工业界正在进行一些努力。该项目将通过确定和填补目前技术水平的一些差距/限制作出额外贡献。从分布式CPS组件的异构行为模型到基于通用自动机的统一模型的转换应该在其他形式推理（例如，监控，模型检查，综合，安全分析）中找到它的用途。研究成果，包括支持软件，将通过公共政策研究所的主页和出版物提供。PI一直在为网络物理系统开发基于模型的方法——设计时（测试和验证）和运行时（监控、诊断和控制），包括使用Simulink/Stateflow开发的响应软件的测试方法，以及此类响应软件的容错方法。对于系统范围的测试和验证，系统级建模语言（AADL或SysML）可以正式捕获端到端的CPS体系结构、组件行为、需求和故障模式。此外，还存在建模和分析工具，包括代码生成器和模型检查器。我们的贡献将是为分布式CPS提供统一系统级建模、测试和验证的新功能，支持新功能：(i) CPS组件建模的新方法，捕获实现缺陷、过程随机性、时序和并发性特征；处理接口和邻近组件模型的方法，以获得供系统级分析的通盘模型；随机动力系统的基于模型的系统级测试方法，引入覆盖率的概率保证和错误定位；（iv）基于成分性质验证的量词消除；混合系统可达性分析的可扩展方法。具体来说，这些将通过以下方式实现：(i)在计算精度和延迟的硬件限制下对软件采用建模方法，以便能够进行早期和成本效益高的循环处理器测试/核查；（ii）对于系统级测试/验证，以通信输入-输出随机混合自动机形式的基于组件的统一并发系统建模，能够捕获定时问题（延迟，漂移，多速率处理），物理组件的随机性和并发性；（iii）考虑到不确定性的系统级测试、验证和错误定位的基于模型的概率方法。采用量词消除法，采用基于组件的设计范例中的成分验证方法；(v)在混合和实时系统中使用迭代的提升和划分，以及在实时系统中使用基于有界模型检查的混合整数线性规划进行可达性分析的新颖可扩展方法。

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.