Over the past years a number of languages and toolsets have been developed for the formal specification and analysis of system behaviour. At this moment, a group of researchers at the Eindhoven University of Technology (the Netherlands) is developing the mCRL2 tool set and language. This language is based on process algebra (ACP, muCRL) and allows for the specification of higher-order data types using lambda-calculus expressions. Using the tool set, labeled transition systems (LTSes, or "state spaces") can be generated from high-level mCRL2 specifications. On these LTSes, model-checking can be performed and visualization techniques can be applied.
In this talk, I will give a short overview of the mCRL2 language and tool set and give examples of case studies in which techniques like mCRL2 have been successful in finding errors in real-life systems or protocols. Next, I will focus on my research project within this context: Visualization of Large Transition Systems (joint work with Hannes Pretorius). In this project, we develop techniques to visualize LTSes (possibly consisting of millions of states) in such a way that a user can gain more insight into the behaviour of the system by interacting with the visualization. I will show you examples of visualizations that have recently been developed in Eindhoven.
| Bas Ploeger |
| Eindhoven University of Technology |
| Date: | Fri Apr 7 2006 |
| Time: | 1:30 to 3pm |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW Kensington campus |
| Convened by: | R.J. van Glabbeek |
Last updated by tbourke at Mon Apr 3 15:25:00 2006 GMT+1000