Tools and Techniques for Integrating Performance Analysis and System Verification

Project code: TIPSyResearch group: Specification and Analysis of Embedded Systems (SEN2) Start: 2003-07-01 End: 2007-06-30 Coordinator of this project: Dr. J.C. van de Pol

Project code: TIPSy
Research group: Specification and Analysis of Embedded Systems (SEN2)

Start: 2003-07-01
End: 2007-06-30

Coordinator of this project: Dr. J.C. van de Pol

In order to combine performance analysis with verification, we will focus on a verification environment for the language Chi. Where necessary we will adapt and enhance existing algorithms for system verification that may include timing and stochastic features. Standard techniques such as partial order reduction, abstraction and symbolic model checking will be employed to fight state explosion. STeP, PVS and a more recently developed theorem prover for the mCRL language will be used to prove invariants and to support equational derivations. This project is a collaboration with the Systems Engineering Group and the Formal Methods Group at Eindhoven University of Technology. The project will be performed in close cooperation with ASML, which committed itself to providing industrial case studies from the realm of production facilities for semiconductors.

Members

Prof.dr. W.J. Fokkink, Dr. J.C. van de Pol, Drs.ing. A.J. Wijs