Abstract
[Motivation] The use of structured natural languages to capture requirements provides a reasonable trade-off between ambiguous natural language and unintuitive formal notations. [Problem] There are two major challenges in making structured natural language amenable to formal analysis: (1) associating requirements with formulas that can be processed by analysis tools and (2) ensuring that the formulas conform to the language semantics. [Results] FRETISH is a structured natural language that incorporates features from existing research and from NASA applications. Even though FRETISH is quite expressive, its underlying semantics is determined by the types of four fields: scope, condition, timing, and response. Each combination of field types defines a template with Real-Time Graphical Interval Logic (RTGIL) semantics. We present an approach that constructs future and past-time metric temporal logic formulas for each template compositionally, from its fields. To establish correctness of our approach we have developed a framework which, for each template: (1) extensively tests the generated formulas against the template semantics and (2) proves equivalence between its past-time and future-time formulas. Our approach has been used to capture and analyze requirements for a Lockheed Martin Cyber-Physical System challenge. [Contribution] To the best of our knowledge, this is the first approach to generate pure past-time and pure future-time formalizations to accommodate a variety of analysis tools. The compositional nature of our algorithms facilitates maintenance and extensibility, and our extensive verification framework establishes trust in the produced formalizations. Our approach is available through the open-source tool fret.
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.
Formal Requirements Elicitation Tool: https://github.com/NASA-SW-VnV/fret.
- 2.
fmLTL with infinite-trace semantics can be produced with a very simple modification to our generation algorithms.
- 3.
Yp is false at the first time point, for all p.
- 4.
Actually the first occurrence of a last time in the mode; see Sect. 4.
- 5.
- 6.
We use clp(fd) in SWI-Prolog: https://www.swi-prolog.org/.
- 7.
Had the scope interval [6..9] been [7..9] instead, the result would have been true for that interval, but still false for the result.
- 8.
Equivalence of formulas was checked with Kind2. [5].
References
Allen, J.F.: Maintaining knowledge about temporal intervals. CACM 26(11), 832–843 (1983)
Badger, J., Throop, D., Claunch, C.: VARED: verification and analysis of requirements and early designs. In: RE 2014, pp. 325–326 (2014)
Bauer, A., Leucker, M.: The theory and practice of SALT. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 13–40. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_3
Bloem, R., Cavada, R., Pill, I., Roveri, M., Tchaltsev, A.: RAT: a tool for the formal analysis of requirements. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 263–267. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_30
Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510–517. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_29
Cobleigh, R.L., Avrunin, G.S., Clarke, L.A.: User guidance for creating precise and accessible property specifications. In: Proceedings of SIGSOFT 2006/FSE 2014. ACM (2006)
Crapo, A., Moitra, A., McMillan, C., Russell, D.: Requirements capture and analysis in ASSERT(TM). In: RE 2017, pp. 283–291 (2017)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE 1999, pp. 411–420. ACM (1999)
Elliott, C.: An example set of cyber-physical V&V challenges for S5. Lockheed Martin Skunk Works. In: Proceedings of S5 2016. AFRL (2016). http://mys5.org/Proceedings/2016/Day_2/2016-S5-Day2_0945_Elliott.pdf
Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: NfM 2017, pp. 420–426 (2017)
Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173–187. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_13
Gallegos, I., Ochoa, O., Gates, A., Roach, S., Salamah, S., Vela, C.: A property specification tool for generating formal specifications: Prospec 2.0. In: SEKE 2008, pp. 273–278 (2008)
Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: ARSENAL: automatic requirements specification extraction from natural language. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 41–46. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_4
Jeannet, B., Gaucher, F.: Debugging embedded systems requirements with STIMULUS: an automotive case-study. In: ERTS 2016 (2016)
Konrad, S., Cheng, B.H.C.: Facilitating the construction of specification pattern-based properties. In: Proceedings of RE 2005, pp. 329–338. IEEE (2005)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proceedings of ICSE 2005, pp. 372–381. ACM (2005)
Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Int. J. Softw. Tools Technol. Transf. 4(2), 224–233 (2003)
Lúcio, L., Iqbal, T.: Formalizing EARS - first impressions. In: 1st International Workshop on Easy Approach to Requirements Syntax (EARS), pp. 11–13 (2018)
Mavin, A.: Listen, then use EARS. IEEE Softw. 29(2), 17–18 (2012)
Mavridou, A., Bourbouh, H., Garoche, P.L., Hejase, M.: Evaluation of the FRET and CoCoSim tools on the ten Lockheed Martin cyber-physical challenge problems. Technical report, TM-2019-220374, NASA (2019)
Moser, L.E., Melliar-Smith, P.M., Ramakrishna, Y.S., Kutty, G., Dillon, L.K.: The real-time graphical interval logic toolset. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 446–449. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61474-5_99
Salamah, S., Gates, A., Roach, S., Mondragon, O.: Verifying pattern-generated LTL formulas: a case study. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 200–220. Springer, Heidelberg (2005). https://doi.org/10.1007/11537328_17
Acknowledgements
We gratefully acknowledge the NASA ARMD System-Wide Safety Project for funding this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 This is a U.S. government work and not under copyright protection in the U.S.; foreign copyright protection may apply
About this paper
Cite this paper
Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J. (2020). Generation of Formal Requirements from Structured Natural Language. In: Madhavji, N., Pasquale, L., Ferrari, A., Gnesi, S. (eds) Requirements Engineering: Foundation for Software Quality. REFSQ 2020. Lecture Notes in Computer Science(), vol 12045. Springer, Cham. https://doi.org/10.1007/978-3-030-44429-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-44429-7_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-44428-0
Online ISBN: 978-3-030-44429-7
eBook Packages: Computer ScienceComputer Science (R0)