VERIFICATION OF COMPLEX HIERARCHICAL SYSTEMS (VOCHS)

The Compact Muon Solenoid (CMS) equipment at CERN is responsible for one of the four experiments in the Large Hadron Collider in Geneva. The software, controlling this experiment, consists of 20,000 to 30,000 finite state machines, which are organised strictly hierarchically. Small constellations of state machines can be verified quite straightforwardly. Verifying the entire system, consisting of such massive numbers of parallel components requires techniques that take full advantage of the hierarchical architecture. The project pursues research in two complementary directions:
  • symbolic verification
  • parallel and distributed verification
The first line of research will be carried out at the TU/e in the Formal System Analysis research group, headed by Prof. Jan Friso Groote, part of the Model-Driven Software Engineering section. The second line of research will be pursued at the UT in the Formal Methods and Tools research group, headed by Prof. Jaco van de Pol. For information on the groups, see:
The detailed project proposal can be downloaded here.


PROJECT MEMBERS

  • Tim Willemse, TU/e, Principle Investigator
  • Maciej Gazda, TU/e, PhD student
  • Gijs Kant, UT, PhD student
  • Rance Cleaveland, University of Maryland
  • Frank Glege, CERN
  • Jan Friso Groote, TU/e
  • Jaco van de Pol, UT



SELECTED PUBLICATIONS

  • M.W. Gazda and T.A.C. Willemse. Consistent Consequence for Boolean Equation Systems. Accepted for SOFSEM 2012.
  • Y.L. Hwong, V.J.J. Kusters and T.A.C. Willemse. Analysing the Control Software of the Compact Muon Solenoid Experiment at the Large Hadron Collider. Accepted for FSEN 2011.
  • S. Cranen, J.J.A. Keiren and  T.A.C. Willemse. Stuttering Mostly Speeds Up Solving Parity Games. In M. Gheorghiu Bobaru, K. Havelund, G.J. Holzmann, R. Joshi (eds.), NASA Formal Methods - Third International Symposium, NFM 2011, Lecture Notes in Computer Science 6617, Springer-Verlag, pp. 207--221, 2011.
  • T.A.C. Willemse. Consistent Correlations for Parameterised Boolean Equation Systems with Applications in Correctness Proofs for Manipulations. In P. Gastin and F. Laroussinie (eds.), Concurrency Theory, 21st International Conference, CONCUR 2010, Paris, France, Lecture Notes in Computer Science 6269, Springer-Verlag, pp. 584--598, 2010.