Abstract
Requirements are informal and semi-formal descriptions of the expected behavior of a complex system from the viewpoints of its stakeholders (customers, users, operators, designers, and engineers). However, for the purpose of design, testing, and verification for critical systems, we can transform requirements into formal models that can be analyzed automatically. ARSENAL is a framework and methodology for systematically transforming natural language (NL) requirements into analyzable formal models and logic specifications. These models can be analyzed for consistency and implementability. The ARSENAL methodology is specialized to individual domains, but the approach is general enough to be adapted to new domains.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
An example of a synthesized Verilog model for the FAA domain is available at: http://www.csl.sri.com/users/shalini/arsenal/faa-isolette.v.
References
Akbik, A., Konomi, O., Melnikov, M.: Propminer: a workflow for interactive information extraction and exploration using dependency trees. In: Proceedings of the ACL: System Demonstrations (2013)
Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueß, H., Rushby, J., Rusu, V., Saïdi, H., Shankar, N., Singerman, E., Tiwari, A.: An overview of SAL. In: LFM (2000)
Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: Automatically extracting requirements specifications from natural language. CoRR abs/1403.3142 (2014)
Li, W., Dworkin, L., Seshia, S.: Mining assumptions for synthesis. In: MEMOCODE (2011)
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)
Quinlan, J.R.: Learning logical definitions from relations. Mach. Learn. 5, 239–266 (1990)
Roth, M., Diamantopoulos, T., Klein, E., Symeonidis, A.: Software requirements: a new domain for semantic parsers. In: Proceedings of the ACL Workshop on Semantic Parsing (2014)
Steiner, W., Dutertre, B.: SMT-based formal verification of a TTEthernet synchronization function. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 148–163. Springer, Heidelberg (2010)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Walter, M.R., Hemachandra, S., Homberg, B., Tellex, S., Teller, S.J.: Learning semantic maps from natural language descriptions. In: Robotics: Science and Systems (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W. (2016). ARSENAL: Automatic Requirements Specification Extraction from Natural Language. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-40648-0_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40647-3
Online ISBN: 978-3-319-40648-0
eBook Packages: Computer ScienceComputer Science (R0)