blob: 48e9328d31da1a2a268f7484396cf13791d52f56 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
\documentclass[runningheads]{llncs}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{cleveref}
\usepackage{csquotes}
\usepackage{minted}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\let\leq\leqslant
\let\le\leqslant
\let\geq\geqslant
\let\ge\geqslant
\DeclareMathOperator{\Uop}{\mathsf{U}}
\newcommand{\PRISM}{\texttt{PRISM}}
\begin{document}
\title{Model Repair in Practice}
\author{Camil Staps \and Erin van der Veen}
\authorrunning{C. Staps \and E. van der Veen}
\institute{%
Radboud University, Nijmegen, The Netherlands\\
\email{\{c.staps,e.vanderveen\}@student.ru.nl}}
\maketitle
\begin{abstract}
We discuss an approach to the repair of parametric models using an SMT solver.
To repair a model $\mathcal M$ which does not satisfy a probabilistic CTL formula $\phi$,
we add an additional parameter to the probability of each transition in $\mathcal M$,
after which we eliminate all non-initial non-absorbing states.
The SMT solver gets constraints to ensure that the repaired model remains valid
and to satisfy $\phi$.
Cost functions for the model repair problem can be formulated as a minimisation goal for the SMT solver.
Unfortunately, some technical issues prevent us from using the tool in practice.
We provide pointers to future work to resolve these issues.
\end{abstract}
\input{intro}
\input{method}
\input{implementation}
\input{discussion}
\input{future}
\bibliography{library}
\bibliographystyle{splncs04}
\end{document}
|
