Cyber-physical systems (CPS) development requires verifying whether system behaviors violate their requirements. This analysis often considers system behaviors expressed by execution traces and requirements expressed by signal-based temporal properties. When an execution trace violates a requirement, engineers need to solve the trace diagnostic problem: They need to understand the cause of the breach. Automated trace diagnostic techniques aim to support engineers in the trace diagnostic activity. This paper proposes search-based trace-diagnostic (SBTD), a novel trace-diagnostic technique for CPS requirements. Unlike existing techniques, SBTD relies on evolutionary search. SBTD starts from a set of candidate diagnoses, applies an evolutionary algorithm iteratively to generate new candidate diagnoses (via mutation, recombination, and selection), and uses a fitness function to determine the qualities of these solutions. Then, a diagnostic generator step is performed to explain the cause of the trace violation. We implemented Diagnosis, an SBTD tool for signal-based temporal logic requirements expressed using the Hybrid Logic of Signals (HLS). We evaluated Diagnosis by performing 34 experiments for 17 trace-requirements combinations leading to a property violation and by assessing the effectiveness of SBTD in producing informative diagnoses and its efficiency in generating them on a time basis. Our results confirm that Diagnosis can produce informative diagnoses in practical time for most of our experiments (33 out of 34).
翻译:信息物理系统(CPS)的开发需要验证系统行为是否违反其需求。该分析通常考虑以执行轨迹表示的系统行为以及以基于信号的时序属性表示的需求。当执行轨迹违反需求时,工程师需要解决轨迹诊断问题:他们需要理解违规的原因。自动化轨迹诊断技术旨在支持工程师进行轨迹诊断活动。本文提出基于搜索的轨迹诊断(SBTD),一种面向CPS需求的新型轨迹诊断技术。与现有技术不同,SBTD依赖于进化搜索。SBTD从一组候选诊断出发,迭代应用进化算法生成新的候选诊断(通过变异、重组和选择),并利用适应度函数评估这些解的质量。随后执行诊断生成步骤以解释轨迹违规的原因。我们实现了Diagnosis工具,这是一个面向使用混合信号逻辑(HLS)表达的基于信号时序逻辑需求的SBTD工具。我们通过34组实验对Diagnosis进行评估,这些实验涵盖17种导致属性违规的轨迹-需求组合,评估内容包括SBTD生成信息性诊断的有效性及其基于时间维度的生成效率。我们的结果表明,在大多数实验案例中(34例中的33例),Diagnosis能够在实际可接受的时间内生成信息性诊断。