Our goal is to use formal methods to reason about systems where time and concurrency play a significant role. We are interested in checking if the behaviours exhibited by an implementation conform to those stipulated by the specification in a timed and distributed system.
To describe the behaviours of distributed systems which operate on a global time, we introduce concrete and abstract notions of message sequence charts (MSCs) with timing. For appropriate formalisms of implementation (timed message passing automata) and specification (monadic second order logic) over timed MSCs, we obtain an expressive equivalence result. Infinite collections of MSCs with timing can also be specified as message sequence graphs with timing. We address two natural problems that arise in this setting.
Finally, we consider an alternate system model where clocks in different components of a distributed system evolve at different local rates. We examine different semantics that allow us to check for good and bad behaviours in the system and show undecidability as well as regularity results.
