Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming

TL;DR

This paper introduces automated techniques combining event calculus and answer set programming to model, validate, and identify gaps in cyber-physical system requirements expressed in natural language, demonstrated on an avionics system.

Contribution

It presents a novel integration of event calculus and ASP for formal modeling and validation of system requirements, enabling automated consistency checks and gap detection.

Findings

Successfully modeled requirements using event calculus

Automated validation of requirements through ASP

Identified gaps in system specifications

Abstract

We consider requirements for cyber-physical systems represented in constrained natural language. We present novel automated techniques for aiding in the development of these requirements so that they are consistent and can withstand perceived failures. We show how cyber-physical systems' requirements can be modeled using the event calculus (EC), a formalism used in AI for representing actions and change. We also show how answer set programming (ASP) and its query-driven implementation s(CASP) can be used to directly realize the event calculus model of the requirements. This event calculus model can be used to automatically validate the requirements. Since ASP is an expressive knowledge representation language, it can also be used to represent contextual knowledge about cyber-physical systems, which, in turn, can be used to find gaps in their requirements specifications. We illustrate our approach through an altitude alerting system from the avionics domain.