Skip to main content
SpringerLink
Log in
Book cover

Brazilian Symposium on Formal Methods

SBMF 2018: Formal Methods: Foundations and Applications pp 252–270Cite as

Formal Modelling of Environment Restrictions from Natural-Language Requirements

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11254))

Abstract

When creating system models, further to system behaviour one should take into account properties of the environment in order to achieve more meaningful models. Here, we extend a strategy that formalises data-flow reactive systems as CSP processes to take into account environment restrictions. Initially, these restrictions are written in natural language. Afterwards, with the aid of case-grammar theory, they are formalised by deriving LTL formulae automatically. Finally, these formulae are used to prune infeasible scenarios from the CSP-based system specification, in the light of the environment restrictions. Considering examples from the literature, and from the aerospace (Embraer) and the automotive (Mercedes) industry, we show the efficacy of our proposal in terms of state space reduction, up to 61% in some cases.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   64.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://patterns.projects.cs.ksu.edu/.

  2. 2.

    https://www.cs.ox.ac.uk/projects/fdr/.

  3. 3.

    https://github.com/Z3Prover/z3.

  4. 4.

    Considering an i7-5500U @ 2.40 GHz 4, 8 GB of RAM, with Ubuntu 16.04 LTS.

  5. 5.

    http://www.embraer.com/en-us/pages/home.aspx.

  6. 6.

    http://www.informatik.uni-bremen.de/agbs/testingbenchmarks/index_e.html.

References

  1. Allerton, D.J.: Valency grammar. In: Brown, K. (ed.) The Encyclopedia of Language and Linguistics, pp. 301–314. Elsevier Science Ltd. (2006)

    Google Scholar 

  2. Carvalho, G.: NAT2TEST: generating test cases from natural language requirements based on CSP. Ph.D. thesis, Centro de Informática, UFPE, Brazil (2016)

    Google Scholar 

  3. Carvalho, G., Barros, F., Carvalho, A., Cavalcanti, A., Mota, A., Sampaio, A.: NAT2TEST tool: from natural language requirements to test cases based on CSP. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 283–290. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_20

    Chapter  Google Scholar 

  4. Carvalho, G., Cavalcanti, A., Sampaio, A.: Modelling timed reactive systems from natural-language requirements. Form. Asp. Comput. 28(5), 725–765 (2016)

    Article  MathSciNet  Google Scholar 

  5. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM, New York (1999)

    Google Scholar 

  6. Fantechi, A., Gnesi, S., Ristori, G., Carenini, M., Vanocchi, M., Moreschini, P.: Assisting requirement formalization by means of natural language translation. Form. Methods Syst. Des. 4(3), 243–263 (1994)

    Article  Google Scholar 

  7. Fillmore, C.J.: The case for case. In: Bach, E., Harms, R.T. (eds.) Universals in Linguistic Theory, pp. 1–88. Holt, Rinehart, and Winston, New York (1968)

    Google Scholar 

  8. Gibson-Robinson, T., et al.: FDR: from theory to industrial application. In: Gibson-Robinson, T., Hopcroft, P., Lazić, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 65–87. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51046-0_4

    Chapter  Google Scholar 

  9. Larsen, K.G., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using Uppaal. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 79–94. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31848-4_6

    Chapter  MATH  Google Scholar 

  10. Leonard, E., Heitmeyer, C.: Program synthesis from formal requirements specifications using APTS. High. Order Symbol. Comput. 16, 63–92 (2003)

    Article  Google Scholar 

  11. Leuschel, M., Currie, A., Massart, T.: How to make FDR spin LTL model checking of CSP by refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 99–118. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45251-6_6

    Chapter  Google Scholar 

  12. Lignos, C., Raman, V., Finucane, C., Marcus, M., Kress-Gazit, H.: Provably correct reactive control from natural language. Auton. Robot. 38(1), 89–105 (2015)

    Article  Google Scholar 

  13. Ma, C., Provost, J.: A model-based testing framework with reduced set of test cases for programmable controllers. In: Proceedings of the IEEE Conference on Automation Science and Engineering, pp. 944–949. IEEE (2017)

    Google Scholar 

  14. Peleska, J., Vorobev, E., Lapschies, F., Zahlten, C.: Automated model-based testing with RT-tester. Universität Bremen, Technical report (2011)

    Google Scholar 

  15. Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13(1), 45–60 (1981)

    Article  MathSciNet  Google Scholar 

  16. Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010). https://doi.org/10.1007/978-1-84882-258-0

    Book  MATH  Google Scholar 

  17. Yan, R., Cheng, C.H., Chai, Y.: Formal consistency checking over specifications in natural languages. In: Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, pp. 1677–1682. EDA Consortium (2015)

    Google Scholar 

Download references

Acknowledgements

This work is partially supported by INES (www.ines.org.br), CNPq grant 465614 /2014-0 and FACEPE grants APQ-0399-1.03/17 and PRONEX APQ/0388-1.03 /14. It is also partially supported by the CIn-UFPE and Motorola cooperation project, as well as by the CNPq grants 303022/2012-4 and 132332/2015-9.

Author information

Authors and Affiliations

  1. Universidade de Pernambuco - Escola Politécnica de Pernambuco, Recife, 50720-001, Brazil

    Tainã Santos

  2. Universidade Federal de Pernambuco - Centro de Informática, Recife, 50740-560, Brazil

    Gustavo Carvalho & Augusto Sampaio

Authors
  1. Tainã Santos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gustavo Carvalho
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Augusto Sampaio
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gustavo Carvalho .

Editor information

Editors and Affiliations

  1. Federal University of Campina Grande, Campina Grande, Brazil

    Tiago Massoni

  2. University of Leicester, Leicester, UK

    Mohammad Reza Mousavi

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Santos, T., Carvalho, G., Sampaio, A. (2018). Formal Modelling of Environment Restrictions from Natural-Language Requirements. In: Massoni, T., Mousavi, M. (eds) Formal Methods: Foundations and Applications. SBMF 2018. Lecture Notes in Computer Science(), vol 11254. Springer, Cham. https://doi.org/10.1007/978-3-030-03044-5_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03044-5_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03043-8

  • Online ISBN: 978-3-030-03044-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation