%0 Conference Paper %1 10.1007/978-3-030-83723-5_3 %A Gros, Timo P. %A Groß, David %A Gumhold, Stefan %A Hoffmann, Jörg %A Klauck, Michaela %A Steinmetz, Marcel %B Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV %C Berlin, Heidelberg %D 2020 %I Springer-Verlag %K Checking Model Networks Neural Statistical Visualization %P 27–46 %R 10.1007/978-3-030-83723-5_3 %T TraceVis: Towards Visualization for Deep Statistical Model Checking %U https://doi.org/10.1007/978-3-030-83723-5_3 %X With the proliferation of neural networks (NN), the need to analyze, and ideally verify, their behavior becomes more and more pressing. Significant progress has been made in the analysis of individual NN decision episodes, but the verification of NNs as part of larger systems remains a grand challenge. Deep statistical model checking (DSMC) is a recent approach addressing that challenge in the context of Markov decision processes (MDP) where a NN represents a policy taking action decisions. The NN determinizes the MDP, resulting in a Markov chain which is analyzed by statistical model checking. Initial results in a Racetrack case study (a simple abstract encoding of driving control) suggest that such a DSMC analysis can be useful for quality assurance in system approval or certification.Here we explore the use of visualization to support DSMC users (human analysts, domain engineers). We implement an interactive visualization tool, TraceVis, for the Racetrack case study. The tool allows to explore crash probabilities into particular wall segments as a function of start position and velocity. It furthermore supports the in-depth examination of the policy traces generated by DSMC, in aggregate form as well as individually. This demonstrates how visualization can foster the effective analysis of DSMC results, and it forms a first step in combining model checking and visualization in the analysis of NN behavior. %@ 978-3-030-83722-8

@inproceedings{10.1007/978-3-030-83723-5_3, abstract = {With the proliferation of neural networks (NN), the need to analyze, and ideally verify, their behavior becomes more and more pressing. Significant progress has been made in the analysis of individual NN decision episodes, but the verification of NNs as part of larger systems remains a grand challenge. Deep statistical model checking (DSMC) is a recent approach addressing that challenge in the context of Markov decision processes (MDP) where a NN represents a policy taking action decisions. The NN determinizes the MDP, resulting in a Markov chain which is analyzed by statistical model checking. Initial results in a Racetrack case study (a simple abstract encoding of driving control) suggest that such a DSMC analysis can be useful for quality assurance in system approval or certification.Here we explore the use of visualization to support DSMC users (human analysts, domain engineers). We implement an interactive visualization tool, TraceVis, for the Racetrack case study. The tool allows to explore crash probabilities into particular wall segments as a function of start position and velocity. It furthermore supports the in-depth examination of the policy traces generated by DSMC, in aggregate form as well as individually. This demonstrates how visualization can foster the effective analysis of DSMC results, and it forms a first step in combining model checking and visualization in the analysis of NN behavior.}, added-at = {2024-11-12T14:55:23.000+0100}, address = {Berlin, Heidelberg}, author = {Gros, Timo P. and Gro\ss{}, David and Gumhold, Stefan and Hoffmann, J\"{o}rg and Klauck, Michaela and Steinmetz, Marcel}, biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/2f62a0606b844fee95e065ca563f29da1/scadsfct}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV}, doi = {10.1007/978-3-030-83723-5_3}, interhash = {94cfe5c3697bdc44a2c47c2a3897ede7}, intrahash = {f62a0606b844fee95e065ca563f29da1}, isbn = {978-3-030-83722-8}, keywords = {Checking Model Networks Neural Statistical Visualization}, location = {Rhodes, Greece}, numpages = {20}, pages = {27–46}, publisher = {Springer-Verlag}, timestamp = {2024-11-12T14:55:51.000+0100}, title = {TraceVis: Towards Visualization for Deep Statistical Model Checking}, url = {https://doi.org/10.1007/978-3-030-83723-5_3}, year = 2020 }