A New Logic Programming Framework for Heterogeneous Verification of Embedded Control Systems

Heterogeneous verification is the integration of verification results from several formal and informal activities using different tools and different models to achieve system-level verification. In previous papers we introduced an ontology- based approach to heterogeneous verification. A static ontology provides a structure for the heterogeneous information and an epistemic ontology provides rules for reasoning about this information. This paper presents our heterogeneous verification tool that implements a new logic programming language EOLC (Epistemic Ontology Language with Constraints) for specifying the epistemic ontology for heterogeneous verification. We describe the features of EOLC and illustrate them for the verification of the mode logic of a redundant flight guidance system.