arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1910.08306eess.SYcs.SY
收藏

用规范变换和赋值布尔函数增强时序逻辑证伪

Enhancing Temporal Logic Falsification with Specification Transformation and Valued Booleans

Johan Lidén Eddeland, Koen Claessen, Nicholas Smallbone, Zahra Ramezani, Sajed Miremadi, Knut Åkesson

摘要:

网络物理系统(CPS)是具有物理和软件组件的系统,例如汽车和工业机器人。由于这些系统表现出离散和连续的动态,它们是复杂的,因此很难验证它们的行为是否符合预期。时序逻辑性质的证伪是通过模拟来寻找CPS反例的一种方法。在本文中,我们提出了两个补充,以提高伪造的能力,使其在大规模的工业环境中更可行。第一个增加的是一个框架,用于将规范从基于信号的模型转换为信号时序逻辑。第二个补充是在证伪过程中使用值布尔和添加剂鲁棒语义。我们评估了一组基准模型上的附加鲁棒语义的性能,我们可以看到,哪些语义是更可取的依赖于模型和规范。

英文摘要:

Cyber-Physical Systems (CPSs) are systems with both physical and software components, for example cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this paper, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into Signal Temporal Logic. The second addition is the use of Valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑