Schedule

Deliverables are defined only for the first two years, and may be subject to later revision. Because we expect a strong interaction between theory and application a precise format of the output in later years will be defined also on the basis of the feedback that we receive.

Year 1


Task A
  • Transformation theory of process algebraic specifications into linear format, including a prototype transformation tool for a subset of muCRL.
  • Efficient, finite McMillan prefix representation for concurrent processes for simulation, model checking, and testing.
  • Proof system for modal properties with data on linear process operators.
Task B
  • Definition of algebraic methods for the specification and analysis of real-time and stochastic concurrent processes.
  • Prototype stochastic simulator for concurrent processes.
Task C
  • Overview of state-of-the-art validation techniques, describing their scope and potential for industrial use.
  • Assessment of the validation project for the BOS/BESW interface system of the Nieuwe Waterweg.
  • Assessment of the verification project for the railway Vital Processor Interlocking at Heerhugowaard.
Task D
  • Establishment of prerequisites for a validation methods tool bench.
  • Assessment of current tool bench developments for applicability within SVC.
  • Integration of the SPIN/Promela model checker in a revision control system.
Task E
  • Introductory course in validation methods and tools for industrial application.
  • Preliminary validation demo centre; presentations and demonstrations of validation methods and tools.

Year 2


Task A
  • Comparative theory of propositional encoding techniques for process analysis.
  • Proof methodology for the validation of modal formulas with data on linear process operators, including prototype verification tool.
  • Methods for combining abstraction and reduction techniques for validation by model checking.
  • State space reduction methods based on the analysis of linear process parameters.
Task B
  • Integration of basic queuing theory in the algebraic methods and tools for the specification and analusis stochastic concurrent processes.
  • Extension of the verification theory for linear process operators to real-time processes.
Task C
  • Revision overview of state-of-the-art validation techniques, describing their scope and potential for industrial use.
  • Worldwide knowledge network of groups that apply validation methods in an industrial setting.
  • Specification and validation of modular car lift system protocols.
  • Application case study (to be selected).
Task D
  • First version of the architecture of the validation tool bench; prototype showing the feasibility of the concept.
  • Definition of muCRL, and possibly LOTOS, with concrete datatypes.
Task E
  • Updated overview of main validation techniques, describing scope and potential for telematics systems.
  • Advanced course in validation methods and tools for industrial application.
  • Establishment validation demo centre with extended set of tools available; presentations and demonstrations of validation methods and tools.

This page was last updated by Holger Hermanns on 2000-03-20