Oct 26, 2010: Gijs Kant: Verification of Complex Hierarchical Systems (VOCHS) Project

October 26, 2010Verification of Complex Hierarchical Systems (VOCHS) Project
Room: Zi 5126Gijs Kant

In this talk the topic of the Verification of Complex Hierarchical Systems (VOCHS) project will be presented. The project aims at improving existing verification methods based on the mCRL2 proces algebra and the mu-calculus for large complex systems. One of the ways to do verification of mCRL2 specifications is to translate a linearised specification together with a mu-calculus formula to a Parameterised Boolean Equation System (PBES), a fixpoint equation system over the boolean lattice, parameterised with data variables. Such a PBES is instantiated (unfolded) into a Boolean Equation System (BES) without data parameters (and quantifiers) or to an equivalent Parity Game. In particular, the project aims at providing more efficient and distributed algorithms for the instantiation of a PBES to a BES, which is similar to generating a LTS. Also, a more modular approach to the verification process has to be developed in order to be able to deal with large and complex systems, using the existing structure/hierarchy of the problem. As a case study an existing large system is used consisting of about 30,000 parallel components.