Time: Wednesday 8.2.2006, 14:30
Place: Room B2-109, Fr. Bajersvej 7
The complexity of modern (computer-)systems makes it impossible to analyse their behaviour. A common way to alleviate this is to build a model of the real system by abstracting away details irrelevant to the analysis. While useful, this approach has at least three problems: how do we go from the real system, how does a domain expert with little or no knowledge of the modeling language validate that the model indeed corresponds to the real system, and, even though the model has simpler behaviour than the real system, it may still be very large or even infinite. During my talk, I will go into solutions for the two latter problems: I will present the tool BRITNeY animation, which makes it possible to create easy to understand visualisations of formal models, which can help domain experts understand the model. I will, also outline the architecture of a state space exploration tool, which makes it easy to experiment with different state space reduction techniques, which alleviate the problem of large state spaces caused by complex behaviours. I will also introduce two new state space reduction techniques.