着色Petri网模型中网的覆盖分析
Coverage Analysis of Net Inscriptions in Coloured Petri Net Models
摘要：
高级Petri网如有色Petri网（CPNs）的特征在于Petri网和高级程序设计语言的结合。在CPN和CPN工具的上下文中，题字（例如，弧表达式和保护）使用标准ML（SML）指定。用于验证CPN模型的模拟和状态空间探索（SSE）的应用传统上集中于与网络结构相关的行为特性，即，地点和过渡。这意味着，净铭文只是隐含的验证，而这些已经覆盖的程度并不明确。本文的贡献是一种方法，它建立了一个覆盖率之间的联系，从程序设计语言和网络铭文的CPN模型的分析。具体来说，我们考虑修改条件/决策覆盖（MC/DC），概括分支覆盖的SML决策。我们已经实现了我们的方法在CPN工具库组成的注释和仪器化机制，透明地拦截和收集布尔条件的评估，和后处理工具，确定是否每个决定是MC/DC覆盖的一组模型执行（运行）。我们评估我们的方法上四个较大的公共可用的CPN模型。
英文摘要：
High-level Petri net such as Coloured Petri Nets (CPNs) are characterised by the combination of Petri nets and a high-level programming language. In the context of CPNs and CPN Tools, the inscriptions (e.g., arc expressions and guards) are specified using Standard ML (SML). The application of simulation and state space exploration (SSE) for validating CPN models traditionally focuses on behavioural properties related to net structure, i.e., places and transitions. This means that the net inscriptions are only implicitly validated, and the extent to which these have been covered is not made explicit. The contribution of this paper is an approach that establishes a link between coverage analysis known from programming languages and net inscriptions of CPN models. Specifically, we consider Modified Condition/Decision Coverage (MC/DC) which generalises branch coverage of SML decisions. We have implemented our approach in a library for CPN Tools comprised of an annotation and instrumentation mechanism that transparently intercept and collect evaluations of Boolean conditions, and a post-processing tool that determines whether each decision is MC/DC-covered by a set of models executions (runs). We evaluate our approach on four larger public-available CPN models.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
