Two-stage agent program verification
Two-stage agent program verification
复制标题
DOI：
10.1093/logcom/exv002
复制
发表时间：
2018-04
期刊：
影响因子：
--
通讯作者：
Louise Dennis;Michael Fisher;M. Webster
中科院分区：
文献类型：
--
作者：
Louise Dennis;Michael Fisher;M. Webster
我们描述了一个扩展AJPF代理程序模型检查器，使它可以用来生成模型输入到其他，非代理，模型检查器。我们激励这种适应，认为它可能会提高模型检查过程的效率，并提供更丰富的属性规范语言。我们通过描述AJPF程序模型到SPIN和Prism模型检查器的导出来说明该方法。我们还调查，实验，该过程对模型检查的整体效率的影响。
We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the modelchecking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and Prism model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.