ARSENAL: Automatic Requirements Specification Extraction from Natural Language

Abstract:

Motivation: Natural language descriptions and formal modeling languages offer distinct advantages to the system designer. Natural language is convenient for succinctly communicating technical descriptions between the stakeholders (e.g., customers, designers, implementers) involved in a design. However, natural language descriptions can be imprecise and ambiguous, and cannot easily be processed by design and analysis tools. Formal languages, on the other hand, can be used to formulate design requirements in a precise and unambiguous mathematical notation, but mastering the use of such notations can require a significant amount of training and mathematical sophistication. We aim to leverage the best of both natural and formal languages, to best support the system designer in achieving high-assurance for critical systems. We propose ARSENAL, a state-of-the-art system to connect stylized natural language descriptions with their precise formal representations, made possible by recent advances in natural language processing (NLP) and formal methods (FM).

Approach: The overall ARSENAL pipeline for converting requirements specification in natural language (semi-structured text format) to formal logical assertions is outlined in Figure 1. The input of ARSENAL consists
of requirements in stylized natural language with specific technical content, including tables and diagrams. We use domain-specific semantic parsing to extract formulas in first-order logic and linear-temporal logic (LTL) from requirements text in the NLP stage. These are then converted to specifications in the FM stage, which can be used by formal verification tools like Theorem provers and SMT solvers (e.g., PVS [1], SAL [2]) as well as LTL synthesis tools (e.g. RATSY [3]) for automated analysis of the formal specifications.

Benefits: Combining natural language requirements with formal representations promotes clear communication among humans at initial phases of the design and implementation of a complex system, enabling early mechanical calculation of important system properties. Among many benefits, ARSENAL enables the user in the following tasks: (1) Removing ambiguities in requirements, (2) Consistency/redundancy checking and validation of requirements, (3) Example generation for test cases, (4) Putative theorem exploration, (5) Traceability to connect implementation to requirements they implement. ARSENAL also helps train engineers in better requirements writing.

Related Work: Related work in this problem include PROPEL [5] and CARL [6]. PROPEL guides the user in writing better requirements but does not extract formulas from requirements automatically like ARSENAL, and also does not do automatic consistency checks between requirements. CARL processes natural language using an entity/relation extractor, and checks consistency between requirements using classical logic and non-monotonic reasoning. In comparison, ARSENAL seamlessly combines state-of-the- art tools of NLP (semantic parsing) and FM (model checking).

Conclusion: ARSENAL is a powerful tool to help a requirements engineer synthesize a more robust and complete formal specification by using informal ones written in stylized natural language, in an interactive process. Thus, ARSENAL allows complex systems to be specified, designed, analyzed, com- posed, and maintained with the aid of natural language artifacts that can be understood by multiple stake-holders. ARSENAL also establishes a growth path to gradually establishing formal methods as mainstream engineering tools, to be used on a daily basis throughout a broad variety of industrial areas and even engineering disciplines.

REFERENCES

[1] S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas, “PVS: combining specification, proof checking & model checking,” in CAV’96.

[2] S. Bensalem, V. Ganesh, Y. Lakhnech, C. M. noz, S. Owre, H. Rueß, J. Rushby, V. Rusu, H. Sa ïdi, N. Shankar, E. Singerman, and A. Tiwari, “An overview of SAL,” in LFM’00.

[3] R.Bloem, A.Cimatti, K.Greimel, G.Hofferek, R.Knighofer,M.Roveri, V. Schuppan, and R. Seeber, “Ratsy a new requirements analysis tool with synthesis,” in CAV’10.

[4] B. Jobstmann and R. Bloem, “Optimizations for LTL synthesis,” in FMCAD’06.

[5] R. L. Smith, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil, “Propel: An approach supporting property elucidation,” in ICSE’02.

[6] D. Zowghi, V. Gervasi, and A. McRae, “Using default reasoning to discover inconsistencies in natural language requirements,” in APSEC’01.