Automated testing of planning models

Klaus Havelund, Alex Groce, Gerard Holzmann, Rajeev Joshi, Margaret Smith

Research output: Contribution to journalConference articlepeer-review

4 Scopus citations


Automated planning systems (APS) are maturing to the point that they have been used in experimental mode on both the NASA Deep Space 1 spacecraft and the NASA Earth Orbiter 1 satellite. One challenge is to improve the test coverage of APS to ensure that no unsafe plans can be generated. Unsafe plans can cause wasted resources or damage to hardware. Model checkers can be used to increase test coverage for large complex distributed systems and to prove the absence of certain types of errors. In this work we have built a generalized tool to convert the input models of an APS to Promela, the modeling language of the Spin model checker. We demonstrate on a mission sized APS input model, that we with Spin can explore a large part of the space of possible plans and verify with high probability the absence of unsafe plans.

Original languageEnglish (US)
Pages (from-to)90-105
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5348 LNAI
StatePublished - 2009
Externally publishedYes
Event5th International Workshop on Model Checking and Artificial Intelligence, MoChArt 2008 - Patras, Greece
Duration: Jul 21 2008Jul 21 2008

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Automated testing of planning models'. Together they form a unique fingerprint.

Cite this