Applications of Goal-directed Answer Set Programming to Avionics Industry* Brendan Hall∗, Sarat Chandra Varanasi†, Jan Fiedor‡, Joaquin Arias§, Kinjal Basu†, Fang Li†, Devesh Bhatt∗, Kevin Driscoll∗, Elmer Salazar†, Gopal Gupta† ∗Honeywell Advanced Technology, Plymouth, USA †Department of Computer Science, The University of Texas at Dallas, Richardson, TX, USA ‡ Honeywell International s.r.o, Brno, Czech Republic & Brno Univ. of Technology §Universidad Rey Juan Carlos, Madrid, Spain Developing effective requirements is crucial for success in 1) How to systematically capture design and intent within building a system. The more complete, consistent, and feasible the MIDAS framework. the requirements, the fewer problems system developers will 2) How ASP-based model checking (over dense time) can encounter later. Current automation of requirements engineer- validate specified system behaviors wrt system properties. ing tasks attempt to ensure completeness, consistency, and 3) How application of abductive reasoning can extend ASP- feasibility. However, such automated support remains limited. based model checking to incorporate domain knowledge In this work, we present novel automated techniques for aiding and real-world/environmental assumptions/concerns. the development of model-augmented requirements that are 4) How knowledge-driven analysis can identify typical re- complete (to the extent possible), consistent, and feasible— quirement specification errors, and/or requirement con- where consistency and feasibility are validated. Thus, we can structs which exhibit areas of potential/probable risk. have more confidence in the requirements. We limit ourselves The talk will be organized as follows. We will give mo- to requirements for cyber-physical systems, particularly those tivation for our work and discuss the importance of writing in avionics. We assume that requirements are generated within requirements that are consistent and complete. We will present the MIDAS (Model-Assisted Decomposition and Specifica- how MIDAS enables a formal flow-down of functional intent tion) [4] environment, and are expressed in CLEAR (Con- through different stages of design refinement. We will sum- strained Language Enhanced Approach to Requirements) [3], marize the two faces of requirements (outward and inward a constraint natural requirement language. facing), as they support validation and verification objectives Our main contribution in this work is to show how the Event (respectively). We will then discuss the enabling background Calculus [5] (EC) and Answer Set Programming (ASP) [2] technologies (EC and ASP), before presenting how they can can be used to formalize constrained natural language require- be integrated within the MIDAS platform to support our goals. ments for cyber-physical systems and perform knowledge- We will illustrate our approach using an altitude alerting case assisted reasoning over them. ASP is a logic-based knowledge study from an actual aerospace system and discuss adjacent representation language that has been prominently used in real-world examples to show how one can use generalized AI. Our work builds upon recent advances made within knowledge within other system contexts. We will illustrate the s(CASP) system [1], a query-driven (or goal-directed) requirement defect discovery using s(CASP) for property- implementation of predicate ASP that supports constraint based model-checking as well as discuss how more general solving over reals, permitting the faithful representation of knowledge of potential requirements defects may detect de- time as a continuous quantity. The s(CASP) system permits fects that traditional techniques may not be able to find. the modeling of event calculus elegantly and directly. A major advantage of using the event calculus—in contrast to automata REFERENCES and Kripke structure-based approaches—is that it can directly [1] Joaqu´ın Arias et al. “Constraint answer set programming model cyber-physical systems, thereby avoiding “pollution” without grounding”. In: TPLP 18(3-4):337-354 (2018). due to (often premature) design decisions that must be made [2] M. Gelfond and Y. Kahl. Knowledge representation, in the other modeling formalisms. The event calculus is a reasoning, & design of intelligent agents: The answer-set formalism—a set of axioms—for modeling dynamic systems programming approach. Cambridge Univ. Press, 2014. and was proposed by artificial intelligence researchers to solve [3] B. Hall, D. Bhatt, et al. “A CLEAR Adoption of EARS”. the frame problem [5]. The primary goal of this work is In: IEEE EARS Workshop. 2018, pp. 14–15. to explore how constrained natural language requirements, [4] B. Hall, J. Fiedor, and Y Jeppu. “Model Integrated specified within MIDAS [4] using the CLEAR notation, can Decomposition and Assisted Specification (MIDAS)”. In: be automatically reasoned about and analyzed using the event INCOSE Int’l Symp. Vol. 30(1):821-841. Wiley. calculus and query-driven answer set programming. Specifi- [5] Murray Shanahan. “The event calculus explained”. In: cally, we explore: Artificial intelligence today. Springer, 1999, pp. 409–430. * Copyright ©2021for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).