Quantitative Model Repair of Stochastic Systems

Modeling and formal verification are among the preliminary steps in system design. Model repair deals with modifying a model in a systematic way whenever it violates a user property related to functional requirements, safety, system performance, availability etc. Modifying a model helps the modeler to fine tune the system as per the needs, instead of redesigning the entire system. After the successful repair, the modified model satisfies the user requirement. The research performed in this thesis proposes effective ways to repair models described as Continuous Time Markov Chains (CTMC), where the user properties are given as Continuous Stochastic Logic (CSL) requirements. The basic idea of our model repair approach is to convert the model into a Parametric Markov Chain (PMC) and synthesize one or several parameters in order to obtain a satisfying solution. In our approach, the PMC contains only a fixed number of parameters, and therefore the parameter synthesis process can be easily scalable for larger systems. To specify the user requirements, we have specified our own version of restricted CSL. The model repair problem for untimed (two cases) CSL requirements is addressed, and we show that the problem for both cases is always solvable. For the time-bounded (four cases) CSL requirements, we show that three out of the total possible four cases are always solvable. In addition, model repair by controller synthesis for Action and State labeled Markov Chains (ASMC) against the CSL with actions and state labels (asCSL) requirements is also addressed. Controllers enforce the desired behavior of a (stochastic) system as per the user needs. Synthesizing appropriate controllers will restrict the behavior of a system and enhances its utilization. During our controller synthesis process, an intermediate model constructed as a product Markov chain should be initially repaired as per the user needs. Therefore, the controller synthesis process internally uses the parameter synthesis algorithms. We address the controller synthesis problem for both the untimed (two cases) and time-bounded (four cases) properties of asCSL, and show that all the cases except one can always be solved.