![[VVPS Workshop]](vvpsws/images/vvpswslogo.png) ![[ICAPS'05]](vvpsws/images/i05-v2.gif) |
|
 Accepted papersPlanning and scheduling (P&S) systems are finding increased application in safety- and mission-critical systems that require a high level of assurance. However, tools and methodologies for verification and validation (V&V) of P&S systems have received relatively little attention. The primary goal of this workshop is to initiate an interaction between the P&S and V&V communities to identify specialized and innovative V&V tools and methodologies that can be applied to P&S. A secondary goal is simply to engage the two communities in the exploration of cross-cutting technologies. Model-based P&S systems have unique architectural features that give rise to new V&V challenges. Most significantly, these systems consist of a planning engine that is largely stable across applications and a declaratively-specified domain model specialized to a particular application. Planners use heuristic search to compute detailed plans that achieve high level objectives stated as an input goal set. Experience has shown that most errors are in domain models, which can be inconsistent, incomplete or inaccurate models of the target domains. There are currently few tools to support the model construction process itself, and even fewer that can be used to validate the structures of the domains once they are constructed. Another challenge to V&V of P&S systems is to demonstrate that specific heuristic strategies have reliable and predictable behaviors. Among the presented papers, some address the topic very directly, by discussing what forms of checks could be performed on plan models. Two papers address how formal methods tools such as a theorem prover and a rewriting system can be applied to model analysis. Two papers target the problem slightly differently and discuss how a real-time model checker can be used as a planning engine, hence giving an understanding of how verification and planning tools relate. The reverse direction is also represented by a paper that discusses how a planning tool can be used for verification. Other papers deal with compositional verification and runtime monitoring. A single paper addresses the synthesis of robust plans, often stated as an alternative approach to correctness. The invited talk by Steve Chien, NASA's Jet Propulsion Laboratory in Pasadena, California, USA, presents work on validating the autonomous EO-1 science agent.
|