Interactive Visualization of Telecommunication Protocol Specs

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.

• Get to know π–Calculus and our tool chain
• Develop an interpreter that creates HTML documents from the Metadata and extracts protocol information from it
• Develop a java applet to interactively display message sequence charts, protocol flaws and process state diagrams

Bachelor of Informatics, Software Systems Engineering or comparable programs.

• Very good knowledge in Java, XML and HTML
• Good understanding of telecommunication protocols, and state machines
• Basic knowledge of Latex