Skip to main content
SpringerLink
Log in

Spatio-Temporal Models for Formal Analysis and Property-Based Testing

  • Conference paper
  • First Online:
Software Technologies: Applications and Foundations (STAF 2016)

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

Abstract

This paper presents our ongoing work on spatio-temporal models for formal analysis and property-based testing. Our proposed framework aims at reducing the impedence mismatch between formal methods and practicioners. We introduce a set of formal methods and explain their interplay and benefits in terms of usability.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

References

  1. Blech, J., Peake, I., Schmidt, H., Kande, M., Rahman, A., Ramaswamy, S., Sudarsan, S., Narayanan, V.: Efficient incident handling in industrial automation through collaborative engineering. In: IEEE 20th Conference on Emerging Technologies Factory Automation (ETFA). IEEE Computer (2015)

    Google Scholar 

  2. Blech, J.O.: An example for BeSpaceD and its use for decision support in industrial automation (2015)

    Google Scholar 

  3. Blech, J.O., Schmidt, H.: BeSpaceD: towards a tool framework and methodology for the specification and verification of spatial behavior of distributed software component systems (2014)

    Google Scholar 

  4. Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods. IEEE Softw. 12(4), 34 (1995)

    Article  Google Scholar 

  5. Broy, M., Stølen, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, New York (2001)

    Book  MATH  Google Scholar 

  6. Charette, R.N.: Why software fails [software failure]. IEEE Spectr. 42(9), 42–49 (2005)

    Article  Google Scholar 

  7. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. ACM SIGPLAN Not. 35(9), 268–279 (2000). doi:10.1145/357766.351266

    Article  Google Scholar 

  8. Dhillon, B.: Engineering Usability: Fundamentals, Applications, Human Factors, and Human Error. American Scientific Publishers, Stevenson Ranch (2004)

    Google Scholar 

  9. Gerdes, A., Hughes, J., Smallbone, N., Wang, M.: Linking unit tests and properties. In: Proceedings of the 14th ACM SIGPLAN Workshop on Erlang, pp. 19–26. ACM (2015)

    Google Scholar 

  10. Hinchey, M.G.: Confessions of a formal methodist. In: Proceedings of the Seventh Australian Workshop Conference on Safety Critical Systems and Software, SCS 2002, vol. 15, pp. 17–20, Australian Computer Society Inc. (2002)

    Google Scholar 

  11. Hordvik, S., Øseth, K., Blech, J.O., Herrmann, P.: A methodology for model-based development and safety analysis of transport systems. In 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE) (2016)

    Google Scholar 

  12. Hu, Z., Hughes, J., Wang, M.: How functional programming mattered. National Sci. Rev. 2(3), 349–370 (2015)

    Article  Google Scholar 

  13. Hughes, J.: Software testing with quickcheck. In: Horváth, Z., Plasmeijer, R., Zsók, V. (eds.) CEFP 2009. LNCS, vol. 6299, pp. 183–223. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17685-2_6

    Chapter  Google Scholar 

  14. Lamport, L.: Hybrid systems in TLA+. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 77–102. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_25

    Chapter  Google Scholar 

  15. Lamport, L.: The temporal logic of actions. ACM Trans. Prog. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  16. Leveson, N.G., Turner, C.S.: An investigation of the therac-25 accidents. Computer 26(7), 18–41 (1993)

    Article  Google Scholar 

  17. Miller, E.: The therac-25 experience. In: Conference on State Radiation Control Program Directors (1987)

    Google Scholar 

  18. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)

    Article  Google Scholar 

  19. Patra, S.: Worst-case software safety level for braking distance algorithm of a train. In: 2007 2nd Institution of Engineering and Technology International Conference on System Safety, pp. 206–210. IET (2007)

    Google Scholar 

  20. Redmill, F., Rajan, J.: Human Factors in Safety-Critical Systems. Butterworth-Heinemann, Oxford (1997)

    Google Scholar 

  21. Spichkova, M.: Human factors of formal methods. In: IADIS Interfaces and Human Computer Interaction, IHCI 2012 (2012)

    Google Scholar 

  22. Spichkova, M.: Design of Formal Languages, Interfaces: Formal Does not Mean Unreadable. IGI Global, Hershey (2013)

    Google Scholar 

  23. Spichkova, M.: Uman factors of formal methods. arXiv preprint arXiv:1404.7247 (2014)

  24. Spichkova, M., Blech, J.O., Herrmann, P., Schmidt, H.W.: Modeling spatial aspects of safety-critical systems with focus-st. In: MoDeVVa@ MoDELS, pp. 49–58, Citeseer (2014)

    Google Scholar 

  25. Spichkova M. et al.,: Specification and seamless verification of embedded real-timesystems: FOCUS on Isabelle. Ph.D. thesis, Technical University Munich (2007)

    Google Scholar 

  26. Spichkova, M., Liu, H., Laali, M., Schmidt, H.W.: Human factors in software reliability engineering. In: Workshop on Applications of Human Error Research to Improve Software Engineering (WAHESE 2015) (2015)

    Google Scholar 

  27. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999). doi:10.1007/3-540-48153-2_6

    Chapter  Google Scholar 

  28. Zamansky, A., Rodriguez-Navas, G., Adams, M., Spichkova, M.: Formal methods in collaborative projects. In: 11th International Conference on Evaluation of Novel Approaches to Software Engineering. IEEE (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. RMIT University, Melbourne, Australia

    Nasser Alzahrani, Maria Spichkova & Jan Olaf Blech

Authors
  1. Nasser Alzahrani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maria Spichkova
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jan Olaf Blech
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nasser Alzahrani .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Universita di Pisa, Pisa, Italy

    Paolo Milazzo

  2. Budapest University of Technology and Economics, Budapest, Hungary

    Dániel Varró

  3. Vienna University of Technology, Vienna, Austria

    Manuel Wimmer

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Alzahrani, N., Spichkova, M., Blech, J.O. (2016). Spatio-Temporal Models for Formal Analysis and Property-Based Testing. In: Milazzo, P., Varró, D., Wimmer, M. (eds) Software Technologies: Applications and Foundations. STAF 2016. Lecture Notes in Computer Science(), vol 9946. Springer, Cham. https://doi.org/10.1007/978-3-319-50230-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-50230-4_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-50229-8

  • Online ISBN: 978-3-319-50230-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation