Modeling and Analyzing Concurrent Systems with Nondeterminism and Time (ciclo LiMoSP)

This talk addresses the great challenge of designing correct concurrent systems, which find many applications in software, hardware, and system design. Formal models of such systems is a prerequisite. We recall the crucial concepts of event-based models, among which concurrency, abstraction, and nondeterminism are essential. We introduce LNT, a modern language for describing such systems and present verification tools for LNT based on model checking and equivalence checking. We then address the case of concurrent systems with time delays modeled using exponential laws, as in Markov chain theory. There are two main approaches to model such systems. In the “integrated” approach each transition carries both an event and a Markovian delay, whereas in the “orthogonal” approach each transition carries either an event or a Markovian delay. Both approaches have been compared by Marco Bernardo et al. on sequential systems. We extend the comparison to the case of concurrent systems by investigating a challenging example, the “Erlangen mainframe”, which features multiple processors, job queues of different priorities, parallel composition with multiway synchronization between two or more concurrent processes, and aperiodic failure/repair events.