=Paper=
{{Paper
|id=Vol-2970/gdeinvited2
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2970/gdeinvited2.pdf
|volume=Vol-2970
}}
==None==
https://ceur-ws.org/Vol-2970/gdeinvited2.pdf
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).