blob: c0a5a8be8a2db9ee4112a19acc1a73cde3523291 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
\section{Future Work}
To get this tool to a usable state,
either Storm needs to be able to read and write parametric DTMCs to DRN files,
or the logic of our tool needs to be re-implemented in Python or C(++) on Storm's data structures.
Either of these options seem to be possible straightforwardly given more knowledge or documentation of Storm.
To implement the cost functions properly, there are different options.
The simplest would be implementing the approximation method described in the previous section.
Another option is to find different kinds of cost functions which can be minimised efficiently.
The present implementation works on DTMCs directly.
It would be more useful to be able to perform model repair on \PRISM\ files directly.
A straightforward way to do this would be to add parameters on the transitions in the \PRISM\ file rather than in the DRN file%
\footnote{This is impossible in the current setup, as Storm cannot generate parameterized DRN files. However, this is no insurmountable problem.}.
Then the instantiations found by Z3 can be used directly to modify the transition probabilities in the \PRISM\ program.
Note however that this method would not resolve all faults, because one transition in a \PRISM\ program may describe several transitions in the DTMC.
To fix such transitions independent from each other, one could add annotations to the DRN format to be able to reconstruct the original \PRISM\ program,
similar to debugging symbols added by a compiler to allow for disassembly.
Then the DRN can be fixed with the solution found by Z3, and the \PRISM\ program can be reconstructed from there.
|
