SPEAKER: Riccardo Traverso

TITLE: Specification and Verification of Concurrent and Distributed Systems

ABSTRACT: Thanks to recent advances in hardware and software architectures, computer systems are more and more dependent on concurrency and distribution: multi-core processors are becoming the default choice even for embedded systems, and wireless devices are spreading in everyday life. The increasing complexity of systems makes testing and verification an even more difficult and challenging problem. My thesis proposal fits in this scenario, starting from this simple observation: usually, individual processes cooperate in a concurrent or distributed system by exploiting or discovering knowledge about their interconnections. Examples can be found at several levels, ranging from cache coherence protocols at the physical layer up to publish/subscribe systems at the application layer. State machines and automata, process calculi, and rewriting systems are examples of widely used approaches to specify and verify concurrent and distributed systems, but the relationships between the communication model and the network topology are not deeply known, especially in conjunction with extensions like, i.e., broadcast communication, mobility, loss of messages and time-dependent constraints. When it comes to analyze a protocol whose behaviour is influenced by the number of nodes and the shape of interconnections, questions about safety properties are related in a natural way to the search for a network topology that enables the protocol to violate the given property. This search for a (possibly arbitrary) connectivity graph easily lifts verification topics from finite-state systems to infinite-state systems, but unfortunately the majority of studies are focused on finite representations. In order to address the aforementioned open problems, the main goal of my work will be the detailed study of (parameterized) verification for concurrent and distributed systems where individual nodes communicate over a network topology, i.e. via (selective) broadcast messages or via rendezvous. More specifically, (1) short-term goals include theoretical studies to define a generic, easy to extend model to be used later, while (2) long-term goals are about searching for useful extensions, effective algorithms and designing/implementing a prototype for infinite-state system verification working with different classes of network topologies, following the guidelines of the generic model.