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.