Automated Model Analysis by State Space Exploration is a postdoc grant 201/07/P035 of Grant Agency of Czech Republic.
Abstract of the proposal: The project focuses on three types of modeling formalisms: extended finite state machines, system dynamics models, and agent based models. These models have applications in the design and verification of computer systems as well as in the study of complex systems. The theme of the project is an automatic analysis of these models by the state space exploration technique. This type of analysis can provide more information about the model than simulation, which is usually used. The goal of the project is to create a database of models, study properties of their state spaces, develop novel techniques of analysis based on state space exploration, implement these techniques and evaluate them. An important part of the project is the effort to syntethise and transfer techniques developed in different application domains.
| Investigator: | Radek Pelánek |
| Collaboration: | ParaDiSe laboratory, particularly Václav Rosecký, Jan Šeděnka, Pavel Šimeček, Jan Krčál, Pavel Moravec, Ondřej Bouda |
| BEEM = BEnchmarks for Explicit Model checkers | A database of models for benchmarking model checkers - models of computer protocols, scheduling problems, puzzles |
| Error detection techniques | Implementation of techniques for error detection (over DiVinE), detailed results of experiments. |
| Memory reduction techniques | Implementation of techniques for reduction of memory consumption (over DiVinE), detailed results of experiments. |
| EMMA tool | Explicit Model checking MAnager; tool for automating the vrification process |