Zervoudakis, F;
(2014)
Cascading Verification: An Integrated Method for Domain-Specific Model Checking.
Doctoral thesis , UCL (University College London).
![[thumbnail of zervoudakis-thesis-final.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) |
PDF
zervoudakis-thesis-final.pdf Download (2MB) |
Abstract
Model checking is an established formal method for verifying the desired behavioral properties of system models. But popular model checkers tend to support low-level modeling languages that require intricate models to represent even the simplest systems. Modeling complexity arises in part from the need to encode domain knowledge, including domain objects and concepts, and their relationships, at relatively low levels of abstraction. We will demonstrate that, once formalized, domain knowledge can be reused to enhance the abstraction level of model and property specifications, and the effectiveness of probabilistic model checking. This thesis describes a novel method for domain-specific model checking called cascading verification. The method uses composite reasoning over high-level system specifications and formalized domain knowledge to synthesize both low-level system models and the behavioral properties that need to be verified with respect to those models. In particular, model builders use a high-level domain-specific language (DSL) to encode system specifications that can be analyzed with model checking. Domain knowledge is encoded in the Web Ontology Language (OWL), the Semantic Web Rule Language (SWRL) and Prolog, which are combined to overcome their individual limitations. Synthesized models and properties are analyzed with the probabilistic model checker PRISM. Cascading verification is illustrated with a prototype system that verifies the correctness of uninhabited aerial vehicle (UAV) mission plans. An evaluation of this prototype reveals non-trivial reductions in the size and complexity of input system specifications compared to the artifacts synthesized for PRISM.
| Type: | Thesis (Doctoral) |
|---|---|
| Title: | Cascading Verification: An Integrated Method for Domain-Specific Model Checking |
| Open access status: | An open access version is available from UCL Discovery |
| Language: | English |
| Keywords: | Composite reasoning, domain model, model checking, OWL, PRISM, Prolog, SWRL, UAVs |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1418833 |
Archive Staff Only
 |
View Item |
