Runtime Verification and Monitoring

[havelund AT email.arc.nasa.gov]

                      Call for Papers

                          VVPS'05

                      1st Workshop on
              Verification and Validation of 
       Model-Based Planning and Scheduling Systems 

          http://planning.cis.strath.ac.uk/vvpsws

                     June 6, 7 - 2005

Held in conjunction with the International Conference on Automated 
Planning and Scheduling, ICAPS 2005, Monterey, CA USA, June 5-10 2005
http://icaps05.icaps-conference.org.


Background

Verification  techniques,   such   as  model  checking,  and  planning
techniques have  many  commonalities.  Planning  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 goal of
this workshop is to initiate an ongoing interaction between the P&S and 
V&V communities, specifically here to  identify   specialized and 
innovative V&V  tools and methodologies that can be applied to P&S.

Model-based P&S systems have unique architectural features that give rise to
new V&V challenges. Most significantly, these systems consist of a planner
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.

While heuristic search has proven effective at finding plans, it is generally
demonstrated only empirically that a given heuristic strategy is effective in
the domains on which it is tried. As planners find wider application and
problems to which they are applied become more adventurous, a second challenge
to V&V in P&S systems is to demonstrate that specific heuristic strategies 
have
reliable and predictable behaviors over their operational profile, including
identification of resource constraints in both the plan generation and in the
quality of the plans produced. 


Organization

In this first workshop, of what it is hoped will become a series of exchanges
between the V&V and P&S communities, we propose to focus on the validation and
verification of domain models. To facilitate contributions on this topic we
make available (on the workshop website) a test bed consisting of a small
collection of domain models. Domains expressed in the standard planning domain
description language PDDL are supplied, together with an account of the
semantics of PDDL, a parser and plan validation tool for PDDL. A planner and
English requirements will also be supplied. Both formal and informal V&V
methods are of interest. 

The workshop will be organized over two days. The first day will be devoted to
presentations of relevant papers, particularly emphasizing work that attempts
to cross the gap between V&V and P&S or proposed approaches to achieving a
greater integration of V&V in P&S. To encourage dialogue and exchange
commentaries will be solicited on all papers that are selected for 
presentation
and presented alongside the primary contributions. The second day will include
an attempt to make practical and concrete headway in the application of V&V
techniques in P&S, in round-table discussions and working groups. 

Important Note: the workshop will have the atmosphere of a working group, 
where
the emphasis is on participation, discussion and exchange of new ideas and not
just on closed form papers (although such are very welcome). This is in
consideration of the novelty of the field, where we encourage new initial 
ideas
and work in process.


Topics of interest include:

- inspection methods, 
- consistency and completeness of domain model, 
- domain model coverage metrics, 
- regression, stress and boundary testing, and
- theoretical foundations.


Submission and publication:

There are two types of submissions: short position statements and regular
papers. Position papers are a maximum of two pages. Regular papers are a
maximum of 12 pages. Papers should be submitted to
icaps05-vvworkshop AT email.arc.nasa.gov
  and should follow the format indicated
on the website. Papers will be printed as a hard-copy hand-out, and workshop
findings and a workshop report will be published on the workshop website.


Important Dates:

Papers due: April 18
Notification of acceptance: May 2
Final papers: May 9


Program Committee: 

Howard Barringer (University of Manchester)
Enrico Giunchiglia (University of Genova)
Tom Henzinger (Ecole Polytechnique Federale de Lausanne)
Gerard Holzmann (JPL/NASA)
Kim Guldstrand Larsen (Aalborg University)
David Musliner (Honeywell)
Nicola Muscettola (NASA Ames)
Douglas Smith (Kestrel Institute)
Carolyn Talcott (SRI)
Brian Williams (MIT)


Chairs: 

Maria Fox (University of Strathclyde)
Allen Goldberg (Kestrel Technology/NASA Ames)
Klaus Havelund (Kestrel Technology/NASA Ames)
Derek Long (University of Strathclyde)