Skip to main content
SpringerLink
Log in

Formal Verification Techniques: A Comparative Analysis for Critical System Design

  • Conference paper
  • First Online:
Intelligent Systems Design and Applications (ISDA 2021)

Part of the book series: Lecture Notes in Networks and Systems ((LNNS,volume 418))

Abstract

Formal methods are used to verify software systems. The system requirements are modeled using specification languages. The models are validated by their tool supports. The Formal methods provide consistency between software development phases and also do the early verification of a system. It provides the blueprint of software. Formal modeling is a rigorous practice in industries. It is used to design systems that are safety, commercial, and mission-critical. This paper presents an in-depth elaboration of some formal verification techniques like Z, B, and Event-B. It also presents a taxonomy of the formal methods in critical system design. Lastly, the specifications are compared with the help of a case study.

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

Similar content being viewed by others

References

  1. Jacky, J.: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, Cambridge (1996)

    Book  Google Scholar 

  2. Abrial, J.R.: The B-Book: Assigning Programs to Meanings by J. R. Abrial. Cambridge University Press, Cambridge (1726)

    Google Scholar 

  3. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)

    Google Scholar 

  4. Karmakar, R., Sarkar, B.B., Chaki, N.: System modeling using Event-B: an insight. In: SSRN Scholarly Paper ID 3511455, Social Science Research Network, Rochester, NY, December 2019

    Google Scholar 

  5. Karmakar, R., Sarkar, B.B., Chaki, N.: Event-B based formal modeling of a controller: a case study. In: Bhattacharjee, D., Kole, D.K., Dey, N., Basu, S., Plewczynski, D. (eds.) Proceedings of International Conference on Frontiers in Computing and Systems. AISC, vol. 1255, pp. 649–658. Springer, Singapore (2021). https://doi.org/10.1007/978-981-15-7834-2_60

    Chapter  Google Scholar 

  6. Karmakar, R., Sarkar, B.B.: A prototype modeling of smart irrigation system using Event-B. SN Comput. Sci. 2(1), 1–9 (2021). https://doi.org/10.1007/s42979-020-00412-8

    Article  Google Scholar 

  7. Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20–38. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00255-7_2

    Chapter  Google Scholar 

  8. Salehi Fathabadi, A., Butler, M.: Applying Event-B atomicity decomposition to a multi media protocol. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 89–104. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17071-3_5

    Chapter  Google Scholar 

  9. Fathabadi, A.S., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Aspects Comput. 27(3), 499–523 (2015)

    Article  MathSciNet  Google Scholar 

  10. Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557–1580 (2013). https://doi.org/10.1007/s10270-013-0391-z

    Article  Google Scholar 

  11. Hvannberg, E.: Combining UML and Z in a Software Process (2001)

    Google Scholar 

  12. Sengupta, S., Bhattacharya, S.: Formalization of UML use case diagram-a Z notation based approach. In: 2006 International Conference on Computing & Informatics, pp. 1–6, Kuala Lumpur, Malaysia. IEEE, June 2006

    Google Scholar 

  13. Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: An overview of RoZ : a tool for integrating UML and Z specifications. In: Wangler, B., Bergman, L. (eds.) CAiSE 2000. LNCS, vol. 1789, pp. 417–430. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-45140-4_28

    Chapter  Google Scholar 

  14. Younes, A.B., Ayed, L.J.B.: Using UML activity diagrams and Event B for distributed and parallel applications. In: 31st Annual International Computer Software and Applications Conference, vol. 1, (COMPSAC 2007), pp. 163–170, Beijing, China. IEEE, July 2007. ISSN: 0730-3157

    Google Scholar 

  15. Snook, C., Butler, M.: UML-B: formal modelling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)

    Article  Google Scholar 

  16. Karmakar, R., Sarkar, B.B., Chaki, N.: Event ordering using graphical notation for Event-B models. In: Saeed, K., Dvorský, J. (eds.) CISIM 2020. LNCS, vol. 12133, pp. 377–389. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-47679-3_32

    Chapter  Google Scholar 

  17. Halder, A., Karmakar, R.: Mapping UML activity diagrams into Z notation. In: Innovative Data Communication Technologies and Application, Proceedings ICIDCA-2021, Lecture Notes on Data Engineering and Communications Technologies. Springer, Cham (2022). ISSN: 2367-4512

    Google Scholar 

  18. Méry, D., Singh, N.K.: Automatic code generation from event-B models. In: Proceedings of the Second Symposium on Information and Communication Technology - SoICT 2011, p. 179, Hanoi, Vietnam, 2011. ACM Press (2011)

    Google Scholar 

  19. Steve, W.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-Based Formal Methods and Tools (2009)

    Google Scholar 

  20. Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for Event-B. Int. J. Softw. Tools Technol. Transfer 19(1), 31–52 (2015). https://doi.org/10.1007/s10009-015-0381-2

    Article  Google Scholar 

  21. Karmakar, R.: A framework for component mapping between Event-B and Python. In: Advances in Data and Information Sciences, Proceedings of RACCCS 2021, Lecture Notes in Networks and Systems. Springer, Cham (2022). https://doi.org/10.1007/978-981-16-7952-0_13

  22. Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 456–471. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_31

    Chapter  Google Scholar 

  23. Guha, S., Nag, A., Karmakar, R.: Formal verification of safety-critical systems: a case-study in airbag system design. In: Abraham, A., Piuri, V., Gandhi, N., Siarry, P., Kaklauskas, A., Madureira, A. (eds.) ISDA 2020. AISC, vol. 1351, pp. 107–116. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71187-0_10

    Chapter  Google Scholar 

  24. Karmakar, R.: Symbolic model checking: a comprehensive review for critical system design. In: Tiwari, S., Trivedi, M.C., Kolhe, M.L., Mishra, K., Singh, B.K. (eds.) Advances in Data and Information Sciences. LNNS, vol. 318. Springer, Singapore (2022). https://doi.org/10.1007/978-981-16-5689-7_62

  25. Abrial, J.-R.: On B and Event-B: principles, success and challenges. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 31–35. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_3

    Chapter  Google Scholar 

Download references

Acknowledgements

I sincerely thank the Department of Computer Science and Engineering, University of Calcutta, India, and Department of Computer Science, The University of Burdwan, India, for their assistance to pursue my research work.

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Burdwan, Burdwan, India

    Rahul Karmakar

Authors
  1. Rahul Karmakar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rahul Karmakar .

Editor information

Editors and Affiliations

  1. Scientific Network for Innovation and Research Excellence, Machine Intelligence Research Labs (MIR Labs), Auburn, WA, USA

    Ajith Abraham

  2. Scientific Network for Innovation and Research Excellence, Machine Intelligence Research Labs (MIR Labs), Auburn, WA, USA

    Niketa Gandhi

  3. Institut für Wirtschaftsinformatik, Fachhochschule Nordwestschweiz, Olten, Switzerland

    Thomas Hanne

  4. Department of Computer Science and information Engineering, National University of Kaohsiung, Kaohsiung, Taiwan

    Tzung-Pei Hong

  5. Federal University of Bahia, Ondina, Brazil

    Tatiane Nogueira Rios

  6. Nantong University, Nantong Shi, Jiangsu, China

    Weiping Ding

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Karmakar, R. (2022). Formal Verification Techniques: A Comparative Analysis for Critical System Design. In: Abraham, A., Gandhi, N., Hanne, T., Hong, TP., Nogueira Rios, T., Ding, W. (eds) Intelligent Systems Design and Applications. ISDA 2021. Lecture Notes in Networks and Systems, vol 418. Springer, Cham. https://doi.org/10.1007/978-3-030-96308-8_9

Download citation

Publish with us

Policies and ethics

Search

Navigation