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
  • Sjoerd Cranen, TU/e, Scientific Programmer/Postdoc
  • Rance Cleaveland, University of Maryland
  • Frank Glege, CERN
  • Jan Friso Groote, TU/e
  • Jaco van de Pol, UT




SELECTED PUBLICATIONS

  • S. Cranen, M.W. Gazda, J.W. Wesselink and T.A.C. Wilemse. Abstraction in Fixpoint Logic. In ACM Transactions on Computational Logic 16(4):29, 2015.

  • S. Cranen, B. Luttik and T.A.C. Willemse, Evidence for Fixpoint Logic. In S. Kreutzer (ed.), CSL 2015, LIPIcs 41, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 78-93, 2015.

  • D. Remenska, T.A.C. Willemse, K. Verstoep, J. Templon and H.E. Bal. Using Model Checking to Analyze the System Behavior of the LHC Production Grid. In Future Generation Computer Systems 29(8):2239-2251, 2013

  • Maciej Gazda and Tim A.C. Willemse, Zielonka’s Recursive Algorithm: dull, weak and solitaire games and tighter bounds. In G. Puppis and T. Villa (eds.), GandALF 2013, Electronic Proceedings in Theoretical Computer Science 119:7-20, 2013.

  • Sjoerd Cranen, Bas Luttik and Tim A.C. Willemse, Proof Graphs for Parameterised Boolean Equation Systems. In P.R. D'Argenio and H. Melgratti (eds.), CONCUR 2013, Lecture Notes in Computer Science 8052, Springer, pp. 470-484, 2013.

  • 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. In Science of Computer Programming 78(12):2435-2452 (2013).

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

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