Department of Computer Science
University of Bologna
4pm Thursday 13th June 2002
Room 2511, JCMB, King's Buildings
A formal approach for the design and analysis of concurrent systems is proposed which integrates two different orthogonal aspects of time: (i) the aspect of probabilistic-time, concerning the probabilistic quantification of durations of system activities via (exponential) probability distributions and the evaluation of system performance, and (ii) the aspect of real-time, concerning the expression of time constraints and the verification of exact time properties. We show that these two aspects, that led to the introduction of different specification paradigms called Markovian process algebras and timed automata, respectively, can be expressed in an integrated way by a single language, namely a process algebra capable of expressing both probabilistic durations and time bounds via probability distributions of a general kind. We will present techniques for system analysis at the level of such an integrated specification as well as formal mappings for obtaining a pure (Markovian) probabilistic-time and a pure real-time system representation which are guaranteed to be consistent and can be analysed by using standard techniques and tools.