Probabilistic model checking (PMC) is a well-established method for the quantitative analysis of dynamic systems. On the other hand, description logics (DLs) provide a well-suited formalism to describe and reason about static knowledge, used in many areas to specify domain knowledge in an ontology. We investigate how such knowledge can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose a formalism that links ontologies to dynamic behaviors specified by guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Further, we present and implement a technique for their analysis relying on existing DL-reasoning and PMC tools. This way, we enable the application of standard PMC techniques to analyze knowledge-intensive systems. Our approach is implemented and evaluated on a multi-server system case study, where different DL-ontologies are used to provide specifications of different server platforms and situations the system is executed in.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:79617 |
| Date | 20 June 2022 |
| Creators | Dubslaff, Clemens, Koopmann, Patrick, Turhan, Anni-Yasmin |
| Publisher | Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:report, info:eu-repo/semantics/report, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:14-qucosa2-785040, qucosa:78504 |
Page generated in 0.0022 seconds