Model checking is used to verify behavior in system models, and Zervoudakis et al. present cascading verification, a novel technique for checking domain-specific models. In particular, formal knowledge of the domain can be used to increase specification abstraction, leading to improved checking effectiveness. Domain knowledge is represented in OWL+SWRL (the web ontology language composed with the semantic web rule language) plus derivative facts encoded in Prolog. This composition provides advantages for overcoming native limitations in the three component languages. Cascading verification is then applied to the domain of unmanned aerial vehicles (UAVs).

The paper is carefully organized and written to accomplish three goals. First, the authors present a new approach for model checking that builds on domain knowledge to reduce the effort associated with specifying systems and their behavioral properties. Second, they describe composite inferencing, which supports the synthesis of system models with their expected behavioral properties as input for probabilistic checking. Third, they discuss a prototype system to demonstrate the new approach to verify mission plans for UAVs. The paper effectively takes a spiral approach that adds insight and depth as aspects of the three goals are revisited. One especially effective diagram (figure 1) lays out processes and data stages that contribute to the overall cascading verification approach and its application.

The authors of this paper have contributed an insightful integrated methodology for domain-oriented model checking that should be of interest to modeling researchers and practitioners. Whether or not it will transfer well to other domains remains open.