On the Formal Semantics of the Cognitive Middleware AWDRAT

The purpose of this work is two fold: on one hand we want to formalize the behavior of critical components of the self generating and adapting cognitive middleware AWDRAT such that the formalism not only helps to understand the semantics and technical details of the middleware but also opens an opportunity to extend the middleware to support other complex application domains of cybersecurity; on the other hand, the formalism serves as a pre-requisite for our proof of the behavioral correctness of the critical components to ensure the safety of the middleware itself. However, here we focus only on the core and critical component of the middleware, i.e. Execution Monitor which is a part of the module "Architectural Differencer" of AWDRAT. The role of the execution monitor is to identify inconsistencies between runtime observations of the target system and predictions of the System Architectural Model. Therefore, to achieve this goal, we first define the formal (denotational) semantics of the observations (runtime events) and predictions (executable specifications as of System Architectural Model); then based on the aforementioned formal semantices, we formalize the behavior of the "Execution Monitor" of the middleware.