Researching formal methods for modeling, verifying and evaluating telecommunication protocols is a project under the UMIC Excellence Cluster at RWTH-Aachen. Telecommunication systems can be viewed as concurrent processes, exchanging messages with each other and evolving over time. In this framework, π–calculus is the model of choice to represent these processes and verify the systems they form. This model has powerful semantic and syntactic features that allow precise description of complex telecommunication systems. However, it is hard to conceive the big picture by reading such models, which also makes detecting and understanding protocol flaws solely by applying analytical means rather challenging. This thesis is intended to visualize these protocol models to ease and simplify the process of studying and analyzing them. This work addresses the problem of interpreting metadata files automatically produced from the π–calculus model and providing a suitable HTML based report. This report displays the text of the model supported with java-applet based protocol diagrams that depict communicating processes, their exchanged messages, and protocol flaws as well.
Bachelor of Informatics, Software Systems Engineering or comparable programs.