On the Behavioural Formalization of the Cognitive Middleware AWDRAT
Muhammad Taimoor Khan, Dimitrios Serpanos, Howard Shrobe

TL;DR
This paper formalizes the behavioral semantics of the AWDRAT middleware's execution monitor to analyze its correctness, which is essential for ensuring the system's security.
Contribution
It introduces a formal denotational semantics for runtime observations and predictions, focusing on the core execution monitor component of AWDRAT.
Findings
Formal semantics of runtime observations defined
Behavior of the execution monitor formalized
Initial results towards correctness analysis obtained
Abstract
We present our ongoing work and initial results towards the (behavioral) correctness analysis of the cognitive middleware AWDRAT. Since, the (provable) behavioral correctness of a software system is a fundamental pre-requisite of the system's security. Therefore, the goal of the work is to first formalize the behavioral semantics of the middleware as a pre-requisite for our proof of the behavioral correctness. However, in this paper, 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 specification System Architectural Model of the system. As a starting point we have defined the formal (denotational) semantics of the observations (runtime…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Distributed and Parallel Computing Systems · Petri Nets in System Modeling
