SpecNFS: A Challenge Dataset Towards Extracting Formal Models from Natural Language Specifications

Proceedings of the 13th Conference on Language Resources and Evaluation (LREC 2022), pages 2166–2176 Marseille, 20-25 June 2022 © European Language Resources Association (ELRA), licensed under CC-BY-NC-4.0 2166 SpecNFS: A Challenge Dataset Towards Extracting Formal Models from Natural Language Specifications Sayontan Ghosh, Amanpreet Singh, Alex Merenstein, Wei Su, Scott A. Smolka, Erez Zadok, and Niranjan Balasubramanian Stony Brook University, Stony Brook, New York {saghosh,amanpsigh,mmerenstein}@cs.stonybrook.edu {suwei,sas,ezk,niranjan}@cs.stonybrook.edu Abstract Can NLP assist in building formal models for verifying complex systems? We study this challenge in the context of parsing Network File System (NFS) specifications. We define a semantic-dependency problem over SpecIR, a representation language we introduce to model sentences appearing in NFS specification documents (RFCs) as semantic dependency structures, and present an annotated dataset of 1,198 sentences. We develop and evaluate semantic-dependency parsing systems for this prob- lem. Evaluations show that even when using a state-of-the-art language model, there is significant room for improvement, with the best models achieving an F1 score of only 60.5 and 33.3 in the named-entity-recognition and dependency-link-prediction sub-tasks, respectively. We also release additional unlabeled data and other domain-related texts. Experiments show that these additional resources increase the F1 measure when used for simple domain-adaption and transfer-learning-based approaches, suggesting fruitful directions for further research. Keywords: specifications dataset, semantic dependency parsing, formal verification 1. Introduction Complex software systems are often designed and im- plemented based on well-defined specifications. A first step towards the formal verification of such a system is to convert its specification, which is often specified in natural language, into a formal model (Soeken et al., 2014). This conversion process is often laborious and error-prone, and a major hindrance to systematic ver- ification of complex systems (Drechsler et al., 2012; Soeken et al., 2014). We ask here if Natural Language Processing (NLP) techniques can assist with automat- ing the process of building formal semantic represen- tations of specification texts. We introduce an instance of this problem in the context of verifying Network File System (NFS) implementations. NFS (Shepler et al., 2008) is a widely used protocol that provides access to files across local and wide- area networks. Implementations of this protocol are expected to meet certain specifications that are de- scribed in detail in what are called RFC (Request for Comment) documents, published by the IETF. These lengthy RFCs (for e.g. NFS RFC 3 is 126 pages long, NFS RFC 4.0 323 pages and NFS RFC 4.1 617 pages long) specify in natural language how each NFS oper- ation must behave under certain inputs and conditions. Verifying an NFS implementation involves building a semantic representation of these specifications, which can then be used to construct formal models. As with any complex system, NFS protocols, imple- mentations, and specifications undergo multiple draft iterations during a multi-year design process, which includes prototype development and regular interoper- ability testing (Viho et al., 2001). Providing tools that can assist with the construction of the formal models can greatly speed up the development and verification of these complex systems. Figure 1: Example specifications …

Content truncated to 500 words