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

  • Y.L. Hwong, J.J.A. Keiren, V.J.J, Kusters, S. Leemans and T.A.C. Willemse. Formalising and Analysing the Control Software of the Compact Muon Solenoid Experiment at the Large Hadron Collider. Accepted for publication in Science of Computer Programming.

  • M. Gazda and T.A.C. Willemse, Expressiveness and Completeness in Abstraction. In B. Luttik and M.A. Reniers (eds.), EXPRESS/SOS, Electronic Proceedings in Theoretical Computer Science 89:49--64, 2012.

  • G. Kant and J. van de Pol. Efficient Instantiation of Parameterised Boolean Equation Systems. In GRAPHITE 2012. To appear.

  • D. Remenska, T.A.C. Willemse, K. Verstoep, W. Fokkink, J. Templon, H. Bal, Using Model Checking to Analyze the System Behavior of the LHC Production Grid. In 12th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2012, pp. 335-343, 2012.

  • M. Gazda and T.A.C. Willemse. Consistent Consequence for Boolean Equation Systems. In M. Bielikova et al. (eds), 38th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2012, Lecture Notes in Computer Science 7147, Springer, pp. 277--288, 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. In F. Arbab, M. Sirjani (eds.), Fundamentals of Software Engineering - 4th IPM International Conference, FSEN 2011, Lecture Notes in Computer Science 7141, pp. 174--189, 2012. Received the Honourable Mention award.

  • 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.