Cyber-Physical Systems (CPSs), comprising both software and physical components, arise in many industry-relevant domains and are often mission- or safety-critical. System-Level Verification (SLV) of CPSs aims at certifying that given (e.g., safety or liveness) specifications are met, or at estimating the value of some KPIs, when the system runs in its operational environment, i.e., in presence of inputs (from users or other systems) and/or of additional, uncontrolled disturbances. To enable SLV of complex systems from the early design phases, the currently most adopted approach envisions the simulation of a system model under the (time bounded) operational scenarios of interest. Simulation-based SLV can be computationally prohibitive (years of sequential simulation), since model simulation is computationally intensive and the set of scenarios of interest can huge. We present a technique that, given a collection of scenarios of interest (extracted from mass-storage databases or from symbolic structures, e.g., constraint-based scenario generators), computes parallel shortest simulation campaigns, which drive a possibly large number of system model simulators running in parallel in a HPC infrastructure through all (and only) those scenarios in the user-defined (possibly random) order, by wisely avoiding multiple simulations of repeated trajectories, thus minimising the overall completion time, compatibly with the available simulator memory capacity. Our experiments on Modelica/FMU and Simulink case study models with up to ~200 million scenarios show that our optimisation yields speedups as high as 8x. This, together with the enabled massive parallelisation, makes practically viable (a few weeks in a HPC infrastructure) verification tasks (both statistical and exhaustive, with respect to the given set of scenarios) which would otherwise take inconceivably long time.

翻译：信息物理系统（CPS）由软件和物理组件组成，出现在许多工业相关领域，且通常具有任务或安全关键性。CPS的系统级验证（SLV）旨在证明系统在其运行环境中（即存在来自用户或其他系统的输入以及/或额外的、不受控的扰动时）满足给定（例如安全或活性）规范，或估计某些关键绩效指标（KPI）的值。为了从早期设计阶段实现复杂系统的SLV，当前最常用的方法是在感兴趣的（时间有界）运行场景下模拟系统模型。基于仿真的SLV可能计算量巨大（需要数年的顺序仿真），因为模型仿真计算密集，且感兴趣的场景集可能非常庞大。我们提出一种技术，给定一组感兴趣的场景（从海量存储数据库或符号结构（例如基于约束的场景生成器）中提取），该技术计算并行的最短仿真活动序列，这些活动以用户定义的（可能为随机）顺序，通过巧妙地避免重复轨迹的多重仿真，驱动可能大量的、在HPC基础设施中并行运行的系统模型模拟器，遍历所有且仅遍历这些场景，从而根据可用模拟器内存容量，最小化整体完成时间。我们在Modelica/FMU和Simulink案例研究模型上的实验（场景数量高达约2亿个）表明，我们的优化可带来高达8倍的加速。结合所支持的大规模并行化，这使得原本需要难以想象的长时间才能完成的验证任务（针对给定场景集的统计验证和穷举验证）在实践上变得可行（在HPC基础设施中仅需数周时间）。