Keynote Speech III: Model Checking with Message Sequence Charts

                           Professor Doron A. Peled, Univ. of Warwick, UK

Abstract:

Message sequence charts is a notation used in practice by
protocol designers and system engineers. In this talk,
some of the recent results related to MSCs,
in the context of specification and automatic verification
of communication protocols, are presented.
We present MSC semantics, checking for race conditions,
model checking, MSC related temporal logics and MSC
extensions.