Two-stage agent program verification. (English) Zbl 1410.68221

Dennis, Louise A.; Fisher, Michael; Webster, Matt

J. Log. Comput. 28, No. 3, 499-523 (2018).

Summary: 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 model-checking 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.

MSC:

68Q60

Specification and verification (program logics, model checking, etc.)

Keywords:

model checking; BDI agent programming; AJPF; SPIN; Prism

Software:

Gwendolen; MCMAS; AJPF; Uppaal; SPIN; PRISM; Java PathFinder; AgentSpeak