[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

VERCORS: Hardware and Software Complex for Intelligent Round-Trip Formalized Verification of Dependable Cyber-Physical Systems in a Digital Twin Environment (Position Paper)

  • Conference paper
  • First Online:
Software Technology: Methods and Tools (TOOLS 2019)

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

Included in the following conference series:

Abstract

Formal specification, model checking and model-based testing are recommended techniques for engineering of mission-critical systems. In the meantime, those techniques struggle to obtain wide adoption due to inherent learning barrier, i.e. it is considered difficult to use those methods. There is also a common difficulty in translating the specifications in natural language, a common practice nowadays, to formal specifications. In this position paper we discuss the concept of an end-to-end methodology that helps identify specifications from various sources, automatically create formal specifications and apply them to verification of cyber-physical systems. Thus, we intent to address the challenges of creation of formal specifications in an efficient automated and tool-supported manner. The novelty of the approach is analyzed through a survey of state of the art. It is currently planned to implement this concept and evaluate it with industrial case studies.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Institutional subscriptions

Similar content being viewed by others

References

  1. Proceedings of IEEE International Symposium on Requirements Engineering, RE 1993, San Diego, California, USA, 4–6 January 1993. IEEE Computer Society (1993)

    Google Scholar 

  2. 25th IEEE International Requirements Engineering Conference, RE 2017, Lisbon, Portugal, 4–8 September 2017. IEEE Computer Society (2017)

    Google Scholar 

  3. Afzal, W., Torkar, R., Feldt, R.: A systematic review of search-based testing for non-functional system properties. Inf. Softw. Technol. 51(6), 957–976 (2009)

    Article  Google Scholar 

  4. Ali, S., Briand, L.C., Hemmati, H., Panesar-Walawege, R.K.: A systematic review of the application and empirical investigation of search-based test case generation. IEEE Trans. Softw. Eng. 36(6), 742–762 (2010)

    Article  Google Scholar 

  5. Antinyan, V., Staron, M., Sandberg, A., Hansson, J.: A complexity measure for textual requirements. In: Heidrich, J., Vogelezang, F.W. (eds.) 2016 Joint Conference of the International Workshop on Software Measurement and the International Conference on Software Process and Product Measurement, IWSM-MENSURA 2016, Berlin, Germany, 5–7 October 2016, pp. 148–158. IEEE Computer Society (2016)

    Google Scholar 

  6. Bakar, N.H., Kasirun, Z.M., Salleh, N.: Terms extractions: an approach for requirements reuse. In: 2015 2nd International Conference on Information Science and Security (ICISS), pp. 1–4, December 2015. https://doi.org/10.1109/ICISSEC.2015.7371034

  7. Bakar, N.H., Kasirun, Z.M., Jalab, H.A.: Towards requirements reuse: identifying similar requirements with latent semantic analysis and clustering algorithms. In: Proceedings of the Second International Conference on Advances In Computing, Communication and Information Technology-CCIT 2014, pp. 19–24 (2014)

    Google Scholar 

  8. Biddle, R., Noble, J., Tempero, E.: Supporting reusable use cases. In: Gacek, C. (ed.) ICSR 2002. LNCS, vol. 2319, pp. 210–226. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46020-9_15

    Chapter  Google Scholar 

  9. Blok, M.C., Cybulski, J.L.: Reusing UML specifications in a constrained application domain. In: 5th Asia-Pacific Software Engineering Conference (APSEC 1998), Taipei, Taiwan, ROC, 2–4 December 1998, pp. 196–202. IEEE Computer Society (1998)

    Google Scholar 

  10. Caron, M., Bäumer, F.S., Geierhos, M.: Back to basics: extracting software requirements with a syntactic approach. In: Schmid et al. [55]

    Google Scholar 

  11. Castano, S., Antonellis, V.D.: Reuse of conceptual requirement specifications. In: Proceedings of IEEE International Symposium on Requirements Engineering, RE 1993, San Diego, California, USA, 4–6 January 1993 [1], pp. 121–124 (1993)

    Google Scholar 

  12. David, A., Larsen, K.G., Li, S., Mikucionis, M., Nielsen, B.: Testing real-time systems under uncertainty. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 352–371. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_19

    Chapter  Google Scholar 

  13. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Boehm, B.W., Garlan, D., Kramer, J. (eds.) Proceedings of the 1999 International Conference on Software Engineering, ICSE 1999, Los Angeles, CA, USA, 16–22 May 1999, pp. 411–420. ACM (1999)

    Google Scholar 

  14. Ferrari, A., dell’Orletta, F., Spagnolo, G.O., Gnesi, S.: Measuring and improving the completeness of natural language requirements. In: Salinesi, C., van de Weerd, I. (eds.) REFSQ 2014. LNCS, vol. 8396, pp. 23–38. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05843-6_3

    Chapter  Google Scholar 

  15. Ferrari, A., Gnesi, S.: Using collective intelligence to detect pragmatic ambiguities. In: Heimdahl, M.P.E., Sawyer, P. (eds.) 2012 20th IEEE International Requirements Engineering Conference (RE), Chicago, IL, USA, 24–28 September 2012, pp. 191–200. IEEE Computer Society (2012)

    Google Scholar 

  16. Ferrari, A., Spagnolo, G.O., Gnesi, S.: PURE: a dataset of public requirements documents. In: 25th IEEE International Requirements Engineering Conference, RE 2017, Lisbon, Portugal, 4–8 September 2017 [12], pp. 502–505 (2017)

    Google Scholar 

  17. Galinier, F., Bruel, J., Ebersold, S., Meyer, B.: Seamless integration of multirequirements in complex systems. In: IEEE 25th International Requirements Engineering Conference Workshops, RE 2017 Workshops, Lisbon, Portugal, 4–8 September 2017, pp. 21–25 (2017)

    Google Scholar 

  18. Garousi, V.: Traffic-aware stress testing of distributed real-time systems based on UML models in the presence of time uncertainty. In: First International Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, 9–11 April 2008, pp. 92–101. IEEE Computer Society (2008)

    Google Scholar 

  19. Harman, M., Jia, Y., Zhang, Y.: Achievements, open problems and challenges for search based software testing. In: 8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, 13–17 April 2015, pp. 1–12. IEEE Computer Society (2015)

    Google Scholar 

  20. Harman, M., Mansouri, S.A., Zhang, Y.: Search based software engineering: a comprehensive analysis and review of trends techniques and applications. Department of Computer Science, King’s College London, Technical report TR-09-03, p. 23 (2009)

    Google Scholar 

  21. Harman, M., Mansouri, S.A., Zhang, Y.: Search-based software engineering: trends, techniques and applications. ACM Comput. Surv. 45(1), 11:1–11:61 (2012)

    Article  Google Scholar 

  22. Harman, M., McMinn, P., de Souza, J.T., Yoo, S.: Search based software engineering: techniques, taxonomy, tutorial. In: Meyer, B., Nordio, M. (eds.) LASER 2008–2010. LNCS, vol. 7007, pp. 1–59. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-25231-0_1

    Chapter  Google Scholar 

  23. Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_3

    Chapter  Google Scholar 

  24. Irshad, M., Petersen, K., Poulding, S.M.: A systematic literature review of software requirements reuse approaches. Inf. Softw. Technol. 93, 223–245 (2018)

    Article  Google Scholar 

  25. Jorgensen, P.C.: The Craft of Model-Based Testing. Auerbach Publications (2017)

    Google Scholar 

  26. Khatibsyarbini, M., Isa, M.A., Jawawi, D.N.A., Tumeng, R.: Test case prioritization approaches in regression testing: a systematic literature review. Inf. Softw. Technol. 93, 74–93 (2018)

    Article  Google Scholar 

  27. Kiyavitskaya, N., Zeni, N., Mich, L., Berry, D.M.: Requirements for tools for ambiguity identification and measurement in natural language requirements specifications. Requir. Eng. 13(3), 207–239 (2008)

    Article  Google Scholar 

  28. Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) 27th International Conference on Software Engineering (ICSE 2005), St. Louis, Missouri, USA, 15–21 May 2005, pp. 372–381. ACM (2005)

    Google Scholar 

  29. Kurtanovic, Z., Maalej, W.: Automatically classifying functional and non-functional requirements using supervised machine learning. In: 25th IEEE International Requirements Engineering Conference, RE 2017, Lisbon, Portugal, 4–8 September 2017 [2], pp. 490–495 (2017)

    Google Scholar 

  30. Maalej, W., Nayebi, M., Johann, T., Ruhe, G.: Toward data-driven requirements engineering. IEEE Softw. 33(1), 48–54 (2016)

    Article  Google Scholar 

  31. McMinn, P.: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab. 14(2), 105–156 (2004)

    Article  Google Scholar 

  32. McMinn, P.: Search-based software testing: past, present and future. In: Fourth IEEE International Conference on Software Testing, Verification and Validation, ICST 2012, Berlin, Germany, 21–25 March, 2011, Workshop Proceedings, pp. 153–163. IEEE Computer Society (2011)

    Google Scholar 

  33. Meyer, B.: On formalism in specifications. IEEE Softw. 2(1), 6–26 (1985)

    Article  Google Scholar 

  34. Meyer, B.: Applying “design by contract”. IEEE Comput. 25(10), 40–51 (1992)

    Article  Google Scholar 

  35. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Upper Saddle River (1997)

    MATH  Google Scholar 

  36. Meyer, B.: Multirequirements. In: Modelling and Quality in Requirements Engineering: Essays dedicated to Martin Glinz on the occasion of his 60th birthday. Verl.-Haus Monsenstein u. Vannerdat (2013)

    Google Scholar 

  37. Naumchev, A.: Detection of inconsistent contracts through modular verification. In: Ciancarini, P., Mazzara, M., Messina, A., Sillitti, A., Succi, G. (eds.) SEDA 2018. AISC, vol. 925, pp. 206–220. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-14687-0_19

    Chapter  Google Scholar 

  38. Naumchev, A.: Object-oriented requirements: reusable, understandable, verifiable. CoRR abs/1903.04165 (2019)

    Google Scholar 

  39. Naumchev, A., Meyer, B.: Complete contracts through specification drivers. In: 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016, Shanghai, China, 17–19 July 2016, pp. 160–167. IEEE Computer Society (2016)

    Google Scholar 

  40. Naumchev, A., Meyer, B.: Seamless requirements. Comput. Lang. Syst. Struct. 49, 119–132 (2017)

    Google Scholar 

  41. Naumchev, A., Meyer, B., Mazzara, M., Galinier, F., Bruel, J.M., Ebersold, S.: Autoreq: expressing and verifying requirements for control systems. J. Comput. Lang. 51, 131–142 (2019)

    Article  Google Scholar 

  42. Naumchev, A., Meyer, B., Rivera, V.: Unifying requirements and code: an example. In: Mazzara, M., Voronkov, A. (eds.) PSI 2015. LNCS, vol. 9609, pp. 233–244. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41579-6_18

    Chapter  Google Scholar 

  43. Niu, N., Savolainen, J., Niu, Z., Jin, M., Cheng, J.C.: A systems approach to product line requirements reuse. IEEE Syst. J. 8(3), 827–836 (2014)

    Article  Google Scholar 

  44. Pacheco, C.L., Garcia, I.A., Calvo-Manzano, J.A., Arcilla-Cobián, M.: Reusing functional software requirements in small-sized software enterprises: a model oriented to the catalog of requirements. Requir. Eng. 22(2), 275–287 (2017)

    Article  Google Scholar 

  45. Paech, B., Martell, C. (eds.): Monterey Workshop 2007. LNCS, vol. 5320. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89778-1

    Book  Google Scholar 

  46. Paydar, S., Kahani, M.: A semantic web enabled approach to reuse functional requirements models in web engineering. Autom. Softw. Eng. 22(2), 241–288 (2015)

    Article  Google Scholar 

  47. Pedersen, N., Lausdahl, K., Sanchez, E.V., Thule, C., Larsen, P.G., Madsen, J.: Distributed co-simulation of embedded control software using INTO-CPS. In: Obaidat, M.S., Ören, T., Rango, F.D. (eds.) SIMULTECH 2017. AISC, vol. 873, pp. 33–54. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-01470-4_3

    Chapter  Google Scholar 

  48. Perednikas, E.: Requirements reuse based on forecast of user needs. In: Proceedings of the 20th EURO Mini Conference on Continuous Optimization and Knowledge-Based Technologies, Neringa, Lithuania, pp. 450–455 (2008)

    Google Scholar 

  49. Periyasamy, K., Chidambaram, J.: Software reuse using formal specification of requirements. In: Bauer, M.A., Bennet, K., Gentleman, W.M., Johnson, J.H., Lyons, K.A., Slonim, J. (eds.) Proceedings of the 1996 conference of the Centre for Advanced Studies on Collaborative Research, Toronto, Ontario, Canada, 12–14 November 1996, p. 31. IBM (1996)

    Google Scholar 

  50. Riebisch, M., Philippow, I., Götze, M.: UML-based statistical test case generation. In: Aksit, M., Mezini, M., Unland, R. (eds.) NODe 2002. LNCS, vol. 2591, pp. 394–411. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36557-5_28

    Chapter  Google Scholar 

  51. Ryan, K.: The role of natural language in requirements engineering. In: Proceedings of IEEE International Symposium on Requirements Engineering, RE 1993, San Diego, California, USA, 4–6 January 1993 [1], pp. 240–242 (1993)

    Google Scholar 

  52. Ryan, K., Mathews, B.: Matching conceptual graphs as an aid to requirements re-use. In: Proceedings of IEEE International Symposium on Requirements Engineering, RE 1993, San Diego, California, USA, 4–6 January 1993 [1], pp. 112–120 (1993)

    Google Scholar 

  53. Sadovykh, A., et al.: SysML as a common integration platform for co-simulations: example of a cyber physical system design methodology in green heating ventilation and air conditioning systems. In: Proceedings of the 12th Central and Eastern European Software Engineering Conference in Russia, CEE-SECR 2016, pp. 1:1–1:5. ACM, New York (2016)

    Google Scholar 

  54. Schlutter, A., Vogelsang, A.: Knowledge representation of requirements documents using natural language processing. In: Schmid et al. [55]

    Google Scholar 

  55. Schmid, K., et al. (eds.): Joint Proceedings of REFSQ-2018 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 23rd International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2018), Utrecht, The Netherlands, 19 March 2018. CEUR Workshop Proceedings, vol. 2075. CEUR-WS.org (2018)

    Google Scholar 

  56. Shafique, M., Labiche, Y.: A systematic review of model based testing tool support (2010)

    Google Scholar 

  57. Sharma, A., Kushwaha, D.S.: Complexity measure based on requirement engineering document and its validation. In: 2010 International Conference on Computer and Communication Technology (ICCCT), pp. 608–615, September 2010

    Google Scholar 

  58. Sutcliffe, A.G., Maiden, N.A.M., Minocha, S., Manuel, D.: Supporting scenario-based requirements engineering. IEEE Trans. Softw. Eng. 24(12), 1072–1088 (1998)

    Article  Google Scholar 

  59. Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566–580. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_53

    Chapter  Google Scholar 

  60. Utting, M., Legeard, B.: Practical Model-Based Testing - A Tools Approach. Morgan Kaufmann, Burlington (2007)

    Google Scholar 

  61. Walden, K., Nerson, J.: Seamless Object-Oriented Software Architecture - Analysis and Design of Reliable Systems. Prentice-Hall, Upper Saddle River (1994)

    Google Scholar 

  62. Walkinshaw, N., Fraser, G.: Uncertainty-driven black-box test data generation. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, 13–17 March 2017, pp. 253–263. IEEE Computer Society (2017)

    Google Scholar 

  63. Weber-Jahnke, J.H., Onabajo, A.: Finding defects in natural language confidentiality requirements. In: RE 2009, 17th IEEE International Requirements Engineering Conference, Atlanta, Georgia, USA, 31 August–4 September 2009, pp. 213–222. IEEE Computer Society (2009)

    Google Scholar 

  64. Yang, H., Willis, A., Roeck, A.N.D., Nuseibeh, B.: Automatic detection of nocuous coordination ambiguities in natural language requirements. In: Pecheur, C., Andrews, J., Nitto, E.D. (eds.) ASE 2010, 25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, Belgium, 20–24 September 2010, pp. 53–62. ACM (2010)

    Google Scholar 

  65. Yoo, S., Harman, M.: Regression testing minimization, selection and prioritization: a survey. Softw. Test. Verif. Reliab. 22(2), 67–120 (2012)

    Article  Google Scholar 

  66. Yue, T., Briand, L.C., Labiche, Y.: A systematic review of transformation approaches between user requirements and analysis models. Requir. Eng. 16(2), 75–99 (2011)

    Article  Google Scholar 

  67. Zhang, M., Ali, S., Yue, T.: Uncertainty-wise test case generation and minimization for cyber-physical systems. J. Syst. Softw. 153, 1–21 (2019). https://doi.org/10.1016/j.jss.2019.03.011. http://www.sciencedirect.com/science/article/pii/S0164121219300561

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Innopolis University, Innopolis, 420500, Russian Federation

    Alexandr Naumchev, Andrey Sadovykh & Vladimir Ivanov

  2. Paul Sabatier University, Toulouse, France

    Alexandr Naumchev

Authors
  1. Alexandr Naumchev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrey Sadovykh
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vladimir Ivanov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexandr Naumchev .

Editor information

Editors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  2. IUT de Blagnac , Blagnac, France

    Jean-Michel Bruel

  3. Innopolis University, Innopolis, Russia

    Bertrand Meyer

  4. Ivannikov Institute for System Programming, Russian Academy of Sciences, Moscow, Russia

    Alexander Petrenko

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Naumchev, A., Sadovykh, A., Ivanov, V. (2019). VERCORS: Hardware and Software Complex for Intelligent Round-Trip Formalized Verification of Dependable Cyber-Physical Systems in a Digital Twin Environment (Position Paper). In: Mazzara, M., Bruel, JM., Meyer, B., Petrenko, A. (eds) Software Technology: Methods and Tools. TOOLS 2019. Lecture Notes in Computer Science(), vol 11771. Springer, Cham. https://doi.org/10.1007/978-3-030-29852-4_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29852-4_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29851-7

  • Online ISBN: 978-3-030-29852-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation