In the engineering of non-functional requirements of a large class of software, hardware, or physical systems, quantitative evaluation of stochastic models enables early assessment of design choices, and provides model driven guidance for implementation and integration stages. In particular, this becomes essential when facing the intertwined effects of concurrency and stochastic timing of systems that are supposed to meet real time requirements.
Most relevant results in the literature of quantitative evaluation have addressed the verification of real-time properties over models with exponentially distributed (EXP) durations. In this case, the underlying stochastic process of the model is a continuous-time Markov chain (CTMC) enabling efficient and mature analysis algorithms. Yet, most systems subject to real time requirement natively include firm timing mechanisms (e.g. timeouts, watchdogs, periodic releases, bounded execution times) that break the assumptions of memoryless and unbounded behavior of EXP variables, and rather require representation of generally distributed (GEN) durations. In this case, the underlying stochastic process of the model falls in more complex classes of so-called non-Markovian processes, for which numerical solution is still to a large extent an open problem.
In this talk, we address the problem of numerical solution of models with concurrent GEN durations, we outline the salient traits of the method of stochastic state classes which significantly enlarges the class of models amenable to numerical solution, and we report on examples of application based on the implementation provided by the Oris tool.
Enrico Vicario is a Full Professor of Computer Science and Engineering (IngInf05 - 09/H1). Since November 2016, he is the Head of the Department of Information Engineering of the University of Florence. He received the PhD in Informatics and Telecommunications Engineering from the University of Florence in 1994.
He works in the area of Software Engineering, with a current scientific focus on quantitative modeling and evaluation of concurrent systems with stochastic durations, and with a practical interest in software architectures and methodologies.
He teaches "Software Engineering" (undergraduate), "Software Architectures and Methodologies" (master), and he is a faculty member of the PhD program in Smart Computing, jointly delivered by the Universities of Florence, Pisa, and Siena.
The lecture series on research talks by the visiting professors of the PhD School can also be credited as an elective course for students of master programs of computer science: TISS