A COMMON FRAMEWORK FOR THE ANALYSIS OF TIMED AND REACTIVE SYSTEMS (COMFORTS)

Model checking is a technique for verifying the designs of real-life systems, including real-time systems, hybrid systems, probabilistic systems and data-dependent systems. The results underlying the techniques from such specialised areas, however, are hard to transfer to other areas because they rely on particular models. Verifying systems that lie in the intersection of two or more domains is often difficult with the currently available techniques.

In this project, we study existing approaches in one framework: Parameterised Boolean Equation Systems (PBESs). This framework is suitable for model checking problems for data-dependent systems. We propose to extend these results to real-time systems, and embed results from specialist areas in the PBESs approach.

Apart from the advantages that are brought about by studying known results in a single framework, PBESs o ffer a novel, and sometimes unique view on the model checking problem. For instance, certain verification problems can be transformed to easier problems, simply by determining the syntactic form of the PBES and looking up its solution. While such techniques are commonplace in mathematics (e.g. for differentiation of functions), they are unique to the field of model checking.




PROJECT MEMBERS

  • Tim Willemse, TU/e, Principle Investigator
  • Simona Orzan, TU/e, Assistant Professor
  • Wieger Wesselink, TU/e, Assistant Professor/Scientific Programmer




SELECTED PUBLICATIONS
  • S.M. Orzan and T.A.C. Willemse. Invariants for Parameterised Boolean Equation Systems. In Theoretical Computer Science, 411(11-13):1338-1371, 2010.
  • T.A.N. Engels, J.F. Groote, M.J. van Weerdenburg and T.A.C. Willemse. Search Algorithms for Automated Validation. In Journal of Logic and Algebraic Programming, 78(4):274-287, 2009.
  • J.J.A. Keiren and T.A.C. Willemse. Bisimulation Minimisations for Boolean Equation Systems. Appeared in Haifa Verification Conference 2009; LNCS post-proceedings will appear in due time.
  • M.A. Reniers and T.A.C. Willemse. Analysis of Structure Graphs for Boolean Equation Systems. In B. Klin and P. Sobocinski (eds.), SOS 2009, Electronic Proceedings in Theoretical Computer Science, 18:92-107, 2010.
  • S.M. Orzan, J.W. Wesselink and T.A.C. Willemse. Static Analysis Techniques for Parameterised Boolean Equation Systems. In S. Kowalewski and A. Philippou (eds.), TACAS 2009, Lecture Notes in Computer Science 5505, pp. 230--245, 2009.
  • S.M. Orzan and T.A.C. Willemse. Invariants for Parameterised Boolean Equation Systems (extended abstract). In F. van Breugel, M. Chechik (eds.), Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, Lecture Notes in Computer Science 5201, Springer-Verlag, pp. 187--202, 2008.
  • A. van Dam, B. Ploeger and Tim A.C. Willemse. Instantiation for Parameterised Boolean Equation Systems. In J.S. Fitzgerald, A.E. Haxthausen, H. Yenigün (eds.), Theoretical Aspects of Computing - ICTAC 2008, 5th International Colloquium, Istanbul, Turkey Lecture Notes in Computer Science 5160, Springer-Verlag, pp. 440--454, 2008.
  • J.F. Groote, J. Keiren, A. Mathijssen, B. Ploeger, F. Stappers, C. Tankink, Y. Usenko, M. van Weerdenburg, W. Wesselink, T. Willemse and J. van der Wulp. The mCRL2 toolset. In Proceedings of the International Workshop on Advanced Software Development Tools and Techniques 2008.
  • T. Chen, B. Ploeger, J. van de Pol and T.A.C. Willemse. Equivalence Checking for Infinite Systems using Parameterized Boolean Equation Systems. In L. Caires, V.T. Vasconcelos (eds.), Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, Lecture Notes in Computer Science 4703, Springer-Verlag, pp. 120--135, 2007.
  • M. Gromov and T.A.C. Willemse. Testing and Model-Checking Techniques for Diagnosis. In A. Petrenko, M. Veanes, J. Tretmans, W. Grieskamp (eds.), Testing of Software and Communicating Systems, 19th IFIP TC6/WG6.1 International Conference, TestCom 2007, 7th International Workshop, FATES 2007, Tallinn, Estonia, Lecture Notes in Computer Science 4581, Springer-Verlag, pp. 138--154, 2007.
  • M. Oostdijk, V. Rusu, J. Tretmans, R.G. de Vries and T.A.C. Willemse. Integrating verification, testing and learning for cryptographic protocols. In J. Davies, J. Gibbons (eds.), Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, Lecture Notes in Computer Science 4591, Springer-Verlag, pp. 538--557, 2007.