ARSENAL: Automatic Requirements Specification Extraction from Natural Language

  • Shalini GhoshEmail author
  • Daniel Elenius
  • Wenchao Li
  • Patrick Lincoln
  • Natarajan Shankar
  • Wilfried Steiner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)


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.


Model Check Linear Temporal Logic Type Rule Bound Model Check Linear Temporal Logic Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: Automatically extracting requirements specifications from natural language. CoRR abs/1403.3142 (2014)Google Scholar
  4. 4.
    Li, W., Dworkin, L., Seshia, S.: Mining assumptions for synthesis. In: MEMOCODE (2011)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Quinlan, J.R.: Learning logical definitions from relations. Mach. Learn. 5, 239–266 (1990)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Shalini Ghosh
    • 1
    Email author
  • Daniel Elenius
    • 1
  • Wenchao Li
    • 1
  • Patrick Lincoln
    • 1
  • Natarajan Shankar
    • 1
  • Wilfried Steiner
    • 2
  1. 1.CSL, SRI InternationalMenlo ParkUSA
  2. 2.TTTech C. AG, Chip IP DesignGrazAustria

Personalised recommendations