Knowledge-Assisted Reasoning of Model-Augmented System Requirements

Presented as part of the 2021 HCSS conference.

ABSTRACT

Developing effective requirements is crucial for success in building a system. The more complete, consistent, and feasible the requirements, the fewer problems system developers will encounter later. Current automation of requirements engineering tasks attempt to ensure completeness, consistency, and feasibility. However, such automated support remains limited. In this work, we present novel automated techniques for aiding the development of model-augmented requirements that are complete (to the extent possible), consistent, and feasible-- where consistency and feasibility are validated. Thus, we can have more confidence in the requirements. We limit ourselves to requirements for cyber-physical systems, particularly those in avionics. We assume that requirements are generated within the MIDAS (Model-Assisted Decomposition and Specification) ^[4] environment, and are expressed in CLEAR (Constrained Language Enhanced Approach to Requirements) ^[3], a constraint natural requirement language.

Our main contribution in this work is to show how the Event Calculus ^[5] (EC) and Answer Set Programming (ASP) ^[2] can be used to formalize constrained natural language requirements for cyber-physical systems and perform knowledge assisted reasoning over them. ASP is a logic-based knowledge representation language that has been prominently used in AI. Our work builds upon recent advances made within the s(CASP) system ^[1], a query-driven (or goal-directed) implementation of predicate ASP that supports constraint solving over reals, permitting the faithful representation of time as a continuous quantity. The s(CASP) system permits the modeling of event calculus elegantly and directly. A major advantage of using the event calculus--in contrast to automata and Kripke structure-based approaches--is that it can directly model cyber-physical systems, thereby avoiding "pollution" due to (often premature) design decisions that must be made in the other modeling formalisms. The event calculus is a formalism--a set of axioms--for modeling dynamic systems and was proposed by artificial intelligence researchers to solve the frame problem ^[5]. The primary goal of this work is to explore how constrained natural language requirements, specified within MIDAS ^[4] using the CLEAR notation, can be automatically reasoned about and analyzed using the event calculus and query-driven answer set programming. Specifically, we explore:

1. How to systematically capture design and intent within the MIDAS framework.
2. How ASP-based model checking (over dense time) can validate specified system behaviors wrt system properties.
3. How application of abductive reasoning can extend ASPbased model checking to incorporate domain knowledge and real-world/environmental assumptions/concerns.
4. How knowledge-driven analysis can identify typical requirement specification errors, and/or requirement constructs which exhibit areas of potential/probable risk.

The talk will be organized as follows. We will give motivation for our work and discuss the importance of writing requirements that are consistent and complete. We will present how MIDAS enables a formal flow-down of functional intent through different stages of design refinement. We will summarize the two faces of requirements (outward and inward facing), as they support validation and verification objectives (respectively). We will then discuss the enabling background technologies (EC and ASP), before presenting how they can be integrated within the MIDAS platform to support our goals. We will illustrate our approach using an altitude alerting case study from an actual aerospace system and discuss adjacent real-world examples to show how one can use generalized knowledge within other system contexts. We will illustrate requirement defect discovery using s(CASP) for property-based model-checking as well as discuss how more general knowledge of potential requirements defects may detect defects that traditional techniques may not be able to find.

REFERENCES

1. Joaqu'in Arias et al. "Constraint answer set programming without grounding". In: TPLP 18(3-4):337-354 (2018).
2. M. Gelfond and Y. Kahl. Knowledge representation, reasoning, & design of intelligent agents: The answer-set programming approach. Cambridge Univ. Press, 2014.
3. B. Hall, D. Bhatt, et al. "A CLEAR Adoption of EARS". In: IEEE EARS Workshop . 2018, pp. 14-15.
4. B. Hall, J. Fiedor, and Y Jeppu. "Model Integrated Decomposition and Assisted Specification (MIDAS)". In: INCOSE Int'l Symp. Vol. 30(1):821-841. Wiley.
5. Murray Shanahan. "The event calculus explained". In: Artificial intelligence today . Springer, 1999, pp. 409-430.

Brendan Hall is an Engineer Fellow with Honeywell Aerospace Advanced Technology. He has over 25 years of experience within safety-relevant domains and has successfully executed internal and externally funded (NASA, AFRL, and FAA) research programs. His research interests include fault-tolerant distributed system architectures, model-based system and safety engineering, formal and property-based design assurance, and the industrial application of formal methods and logic programming. Mr. Hall holds over 45 patents and has published numerous technical papers within the fields of fault-tolerant distributed systems, requirement engineering, applied formal methods, and model-based engineering.

Sarat Chandra Varanasi is a PhD student in the CS Department at UT Dallas. Sarat Chandra's research work involves automatically synthesizing concurrent programs using commonsense knowledge about concurrency. Given a sequential program for a pointer data structure (e.g., insert a node, delete a node), the goal of this research is to automatically synthesize its concurrent version, just like a human would. To accomplish this, knowledge that models concurrency, shared memory, and how pointer data structures behave is used (represented as axioms in answer set programming). Sarat also has several years of industry experience and interests are in distributed computing, concurrency, computational logic, and automated reasoning.

Jan Fiedor is a Model-based development engineer at Honeywell International s.r.o. and an external researcher at Brno University of Technology. He obtained his Ph.D. in the area of software safety analysis, focusing on dynamic analysis of concurrent programs, where he is continuing his work in various European projects. At Honeywell, he is broadening his focus to model-based system and safety engineering, applying his knowledge from the software world to the general system context. He strongly believes that the collaboration between academia and industry will move the world forward.

Joaquin Arias is an assistant professor at Universidad Rey Juan Carlos in Madrid (URJC). He obtained his M.Arch. in Architecture in 2002, his B.Sc./M.Sc. degrees in Informatics in 2014/2015, and received a Ph.D. in Computer Science in 2020, from the Universidad Politecnica de Madrid. His principal area of expertise is the development and application of advanced evaluation techniques for (non-)monotonic reasoning using rules and constraints. His background includes the implementation of an abstract interpreter based on tabled constraint logic programming, and the development (in collaboration with the IMDEA Software Institute and the University of Texas at Dallas) of s(CASP) a novel non-monotonic reasoner that evaluates constraint answer set programs. He is currently a fellow of the Artificial Intelligence Research Group at the URJC and his research interests are in the areas of Event Calculus, XAI, and Building Information Modeling.

Kinjal Basu is a computer science Ph.D. student working under Prof. Gopal Gupta on closed domain question-answering and commonsense reasoning. Currently, he is leading the CASPR team from UT Dallas at the 'Alexa Prize: Social Bot Grand Challenge 4' competition organized by Amazon. His research interest lies in Logic Programming, Natural Language Understanding, and Machine Learning, and his recent papers are in the area of textual and visual question answering and conversational agents. Kinjal also acquired real-world data science project experience while working as an intern at Intuit. During his Bachelor's in Information Technology, he worked on several NLP projects (e.g., Text Similarity) and also interned at IIT Kharagpur for NLP research.

Fang Li is a Computer Science PhD candidate in Prof. Gopal Gupta's lab. Fang's research interests are explainable AI, commonsense reasoning, answer set programming, and logic programming. Fang got his Master' in Applied Mathematics & Computer Science and graduated with honors from University of Central Oklahoma. In the past few years he has conducted research on human computer interaction, IoT, autonomous vehicles, AI planning, and answer set programming implementation. He cofounded a company as a CTO called Turning Systems that won an award in an entrepreneurship competition.

Devesh Bhatt received a B.Tech. in electrical engineering from Indian Institute of Technology Kanpur in 1975 and Ph.D. in EE/CS from Stony Brook University in 1980. He is currently a Senior Fellow at Honeywell Aerospace Laboratories. His research interests include verification of complex safety-critical systems and software, including requirements engineering, analysis, and testing techniques, and certification approaches for use of new technologies in autonomous applications.

Kevin Driscoll is a Fellow at Honeywell Labs with 49 years' experience in safety and security critical systems -- including the aspects of hardware, software, and system design. He currently is leading an $8M effort to create assurance cases. Other recent programs include "Considerations in Assuring Safety of Increasingly Autonomous Systems", "Validation and Verification of Safety-Critical Integrated Distributed Systems", and "Cyber Safety and Security for Reduced Crew Operations". He was a main author of several embedded system network standards and the FAA network selection handbook. Kevin is a consultant to other Honeywell divisions for dependable computing, electronic architectures, and data networks. Kevin has over 50 patents and numerous publications covering safety and security critical real-time systems.

Elmer Salazar is an assistant professor of instruction at the University of Texas at Dallas. Though teaching full time, he dedicates time to research, and works with the ALPS research group. His research interests include non-monotonic computational logic, the application of computational logic to AI and common sense reasoning, and the interaction of machine learning techniques (neural networks) and computational logic. He is the co-designer of the s(ASP) language (a non-monotonic, ungrounded, goal-directed logic programming language based on stable model semantics), and recently has been working on using proof trees generated by proof-theoretic execution to automatically find possible problems in ASP code based on some requirements encoded as predicates.

Gopal Gupta is a professor of computer science at the University of Texas at Dallas where he holds the Erik Jonsson chair. His areas of research interest are in automated reasoning, logic programming, machine learning, programming languages, and assistive technology. He has published extensively in these areas. His group has also authored many software systems, many of which are publicly available. His research work has also resulted in commercial software systems that have formed the basis of two startup companies. His group has won several best-paper awards as well as the ICLP 2016 most influential paper award for their work on co-inductive logic programming. Prof. Gupta's current research is funded by the NSF and DARPA. His lab is one of nine labs worldwide currently competing in the Amazon Alexa Socialbot competition where the goal is to build an Alexa skill that can hold a casual conversation with a random user for at least 20 minutes. He obtained his MS & PhD degrees from UNC Chapel Hill and his B.Tech. in Computer Science from IIT Kanpur, India.