有色Petri网模型中网 inscription 的覆盖分析
软件工程
2020-05-21 v1
摘要
高级Petri网（如有色Petri网，CPN）的特点在于Petri网与高级编程语言的结合。在CPN及CPN Tools语境下，inscription（例如弧表达式与守卫）使用Standard ML（SML）指定。将模拟与状态空间探索（SSE）用于验证CPN模型传统上聚焦于与网结构相关的行为属性，即库所与变迁。这意味着网inscription仅被隐式验证，而其被覆盖的程度并未显式呈现。本文的贡献是一种在编程语言中已知的覆盖分析与CPN模型网inscription之间建立联系的方法。具体而言，我们考虑修正条件/判定覆盖（MC/DC），它推广了SML判定的分支覆盖。我们已在CPN Tools的一个库中实现该方法，该库包含一种标注与插桩机制，可透明地拦截并收集布尔条件的求值结果，以及一个后处理工具，用于判定每组模型执行（运行）是否实现了各判定的MC/DC覆盖。我们在四个较大的公开可用CPN模型上评估了我们的方法。
引用
@article{arxiv.2005.09806,
title = {Coverage Analysis of Net Inscriptions in Coloured Petri Net Models},
author = {Faustin Ahishakiye and José Ignacio Requeno Jarabo and Lars Michael Kristensen and Volker Stolz},
journal= {arXiv preprint arXiv:2005.09806},
year = {2020}
}
备注
Technical Report