Formal Quantitative Analysis of Role-based Systems
Role-based modeling is a promising approach to cope with the context-dependence and the (self-) adaptivity of modern software systems. However, dynamic role changes at runtime may introduce unforeseen and unwanted side effects, like deadlocks or objects acquiring conflicting roles. As today’s society becomes more and more dependent on software systems, reliability, dependability and overall quality are major concerns. Thus, formal methods for modeling, verification and analysis are highly desirable.
Probabilistic Model Checking (PMC) is a formal technique for functional and quantitative analysis. It allows to reason about the probabilities of certain properties, e.g., the probability that an object always plays the same role or the probability that a specific role change leads to a system failure. Furthermore, the quantitative analysis with respect to different utility and cost functions, such as energy consumption, throughput, latency and performance, is also possible. Being able to model stochastic phenomena and environments is especially important for analyzing context-dependent systems. Well known model-checking approaches require a formalization of the system under consideration and the desired requirements. However, to the best of my knowledge, there are currently no formalisms and modeling languages suitable for PMC that incorporate both the context-dependent and collaborative characteristics of role-based systems.
The goal of the thesis is to develop operational models for role-based software infrastructures that allow for quantitative analysis by means of PMC. These models should capture stochastic information about dynamic role changes, their costs and their effects on the system. A major challenge is to find composition operators for the role-based operational models that adequately formalize interactions of role-playing objects. Further steps include the development of suitable modeling languages and model-checking algorithms, as well as the investigation of practical applicability of the developed formalisms and algorithms.