UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Cascading Verification: An Integrated Method for Domain-Specific Model Checking

Zervoudakis, F; (2014) Cascading Verification: An Integrated Method for Domain-Specific Model Checking. Doctoral thesis , UCL (University College London). Green open access

[img] 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
Downloads since deposit
266Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item