Deriving Formal Specifications from Natural Language Requirements using ARSENAL 2

Presented as part of the 2019 HCSS conference.

Requirements specifications for systems, protocols, procedures, and standards are typically written in unstructured text or semi-structured formats for human consumption. These specifications lack the precision needed to support the application of formal tools for analyzing properties of the specification, including consistency and completeness, and for synthesising reference implementations and test cases. Formalizing informal requirements is a critical part of automated software certi-fication.

At SRI, we have been developing ARSENAL as a system for translat-ing informal specifications into formal models that can be analyzed for inconsistency, incompleteness, ambiguity, and errors. The main goal of ARSENAL is to assist specifiers and system designers in developing precise and correct requirements specifications that are humanly readable (by the concerned stakeholders) and amenable to formal modeling and analysis. ARSENAL also enables continuous checking of natural lan-guage requirements as the system specifications and design documents evolve. We have recently developed the ARSENAL 2 prototype based on the novel approach of employing a generative model for natural language to train a machine learning pipeline to generate candidate formulas and models from natural language input. The system features an Inte-grated Development Environment (IDE) for transforming natural language requirements into model checkable system models with animated counterexamples. The ARSENAL 2 approach can be easily ported to other domains. We outline the basic approach employed by ARSENAL 2, summarize the experimental results, and explore the applicability of our approach to other natural language processing tasks.

Joint work with Daniel Elenius, Eric Yeh, Shalini Ghosh, and Pat Lincoln.

Dr. Natarajan Shankar is a Distinguished Scientist at the SRI International Computer Science Laboratory where he and his colleagues have developed a number of widely used formal tools and techniques for hardware and software design, including the PVS proof assistant, the SAL model checker, the Yices SMT solver, the Probabilistic Consistency Engine (PCE), the Occam software debloater, and the Evidential Tool Bus. He is the co-winner of the 2012 CAV Award and was made SRI Fellow in 2009.