Communication protocols constitute critical building blocks in most modern ICT systems as they define components, rules, and languages that make data communication possible. The development of correct communication protocols is a challenging engineering discipline, making modelling and validation of protocols a key application domain for the use of Petri nets, concurrency theory, and model checking technology. The lectures on this topic will provide a brief introduction to Coloured Petri Nets (CPNs), Time Petri Nets (TPNs), and Timed Automata (TA) as languages for constructing formal models of protocols. Next, the use of explicit state space exploration for verification of protocols will be covered. This will be followed by a presentation of the basic approaches to model checking of properties expressible in (timed) temporal logics, focussing on symbolic SAT-based verification. Throughout the lectures, a number of standard and larger industrial case studies will be used to illustrate how the presented modeling languages and associated verification techniques can be applied for the practical verification of protocols.
The following papers are suggested as background material for the lectures:
A comprehensive coverage of the lecture topics can be found in the following textbooks:
The following exercises are suggested for the practical work with CPN Tools. The exercises are taken from the CPN book web page.
It is recommended to work on the exercises in the order listed above. There may not be sufficient time at the practical work to complete all the exercises.
Wojciech Penczek is Professor in Computer Science and the head of the Theory of Distributed Systems group at ICS PAS, Warsaw, Poland. He was a research fellow at the Technical University of Eindhoven and Manchester University; he also worked as a consultant at AT&T. His research is now focused on verification methods for Petri nets , timed automata, and multi-agent systems. He has recently co-authored a book on verificaition of Time Petri Nets and Timed Automata, published by Springer-Verlag . He has been a project leader of the EC-founded project CRIT-2 and played a main role in several national projects. He has chaired and was a PC member of many conferences on Computer Science. He is the author of more than 120 conference and journal articles on temporal logic, verification methods, model checking, and formal theories of concurrency. His teaching record, besides numerous regular undergraduate courses, includes two courses at EASSS (European Agent Systems Summer School). This year he was a co-chair of the Petri Net conference in Braga, Portugal.
Lars Michael Kristensen is Professor in Informatics and director of the software technologies for distributed systems research program at Bergen University College, Norway. He holds a PhD degree in computer science from Aarhus University in 2000, and has previously held positions at University of South Australia and Aarhus University. He has more than 10 years of research experience in the application of state space methods for verification of communication protocol. A main focus has been the theoretical foundation of state space methods and their implementation in computer tools, in particular in the context of Coloured Petri Nets. A strong focus has also been on applying the developed state space methods and supporting computer tools in industrial cooperation projects, in particular in the domain of Internet protocols. He has recently co-authored a new textbook on Coloured Petri Nets published by Springer-Verlag, and in 2007 he received the Danish Independent Research Councils' Young Researcher's Award.