Skip to main content
SpringerLink
Log in

UMC4M: A Verification Tool via Program Execution

  • Conference paper
  • First Online:
Structured Object-Oriented Formal Language and Method (SOFL+MSVL 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12028))

  • 519 Accesses

Abstract

Most of the software model checkers available for code level verification can only verify safety properties since desired properties are specified by assertions. However, other temporal properties such as liveness cannot be verified with these tools. To tackle this problem, we develop a verification tool called UMC4M to verify full regular temporal properties of programs. UMC4M takes a modeling, simulation and verification language (MSVL) program M and a desired property specified by a propositional projection temporal logic (PPTL) formula P as its input. \(\lnot P\) is then translated to an MSVL program M. Thus, the property can be verified by checking whether there is an acceptable execution of “\(M~and~M'\)”, which can be solved with MSVL compiler MC. Further, UMC4M is used to verify the dining cryptographers protocol.

This research is supported by School Funds of Hebei University (No. 299) and Advanced Talents Incubation Program of the Hebei University (No. 521000981346).

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. Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transfer 11(1), 69–83 (2009)

    Article  Google Scholar 

  2. Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 102–122. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45139-0_7

    Chapter  Google Scholar 

  3. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: applications to software engineering. Int. J. Softw. Tools Technol. Transfer 9(5), 505–525 (2007)

    Article  Google Scholar 

  4. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  5. Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_22

    Chapter  Google Scholar 

  6. Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the Sixth Conference on Computer Systems (EuroSys 2011), pp. 183–198. ACM, New York (2011). https://doi.org/10.1145/1966445.1966463

  7. Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1(1), 65–75 (1988)

    Article  MathSciNet  Google Scholar 

  8. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  9. Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 415–426. ACM, New York (2006)

    Google Scholar 

  10. Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49–66. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_4

    Chapter  Google Scholar 

  11. Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, Department of Computer Science, Newcastle University, Newcastle upon Tyne, UK (1996)

    Google Scholar 

  12. Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)

    Google Scholar 

  13. Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19(3), 341–351 (2004)

    Article  MathSciNet  Google Scholar 

  14. Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169–190 (2014)

    Article  MathSciNet  Google Scholar 

  15. Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)

    Article  MathSciNet  Google Scholar 

  16. Duan, Z., Tian, C., Zhang, N.: A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor. Comput. Sci. 609, 544–560 (2016)

    Article  MathSciNet  Google Scholar 

  17. Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Prog. 70(1), 31–61 (2008)

    Article  MathSciNet  Google Scholar 

  18. Havelund, K., Rosu, G.: Monitoring java programs with java pathexplorer. Electron. Notes Theor. Comput. Sci. 55(2), 200–217 (2001)

    Article  Google Scholar 

  19. Kroening, D., Tautschnig, M.: CBMC–C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26

    Chapter  Google Scholar 

  20. Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27705-4_12

    Chapter  Google Scholar 

  21. Navabpour, S., et al.: RiTHM: a tool for enabling time-triggered runtime verification for c programs. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 603–606. ACM, New York (2013)

    Google Scholar 

  22. Tian, C., Duan, Z., Duan, Z., Ong, C.H.L.: More effective interpolations in software model checking. In: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, pp. 183–193. IEEE Press (2017)

    Google Scholar 

  23. Tian, C., Duan, Z., Duan, Z.: Making cegar more efficient in software model checking. IEEE Trans. Softw. Eng. 40(12), 1206–1223 (2014)

    Article  Google Scholar 

  24. Wang, H., Duan, Z., Tian, C.: Model checking multi-agent systems with APTL. Adhoc Sens. Wireless Netw. 37, 35–52 (2017)

    Google Scholar 

  25. Wang, M., Tian, C., Zhang, N., Duan, Z.: Verifying full regular temporal properties of programs via dynamic program execution. IEEE Trans. Reliab. 68, 1–16 (2018)

    Google Scholar 

  26. Yang, K., Duan, Z., Tian, C., Zhang, N.: A compiler for MSVL and its applications. Theor. Comput. Sci. 749, 2–16 (2018)

    Article  MathSciNet  Google Scholar 

  27. Yang, X., Duan, Z.: Operational semantics of framed tempura. J. Logic Algebraic Program. 78(1), 22–51 (2008)

    Article  MathSciNet  Google Scholar 

  28. Yu, B., Duan, Z., Tian, C., Zhang, N.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118, 89–99 (2018)

    Article  Google Scholar 

  29. Zhang, N., Duan, Z., Tian, C.: A mechanism of function calls in MSVL. Theor. Comput. Sci. 654, 11–25 (2016)

    Article  MathSciNet  Google Scholar 

  30. Zhang, N., Duan, Z., Tian, C.: Model checking concurrent systems with MSVL. Sci. China Inf. Sci. 59(11), 118101 (2016)

    Article  Google Scholar 

  31. Zhang, N., Yang, M., Gu, B., Duan, Z., Tian, C.: Verifying safety critical task scheduling systems in PPTL axiom system. J. Comb. Optim. 31(2), 577–603 (2016)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cyberspace Security and Computer College, Hebei University, Baoding, 071000, China

    Meng Wang, Junfeng Tian & Hong Zhang

Authors
  1. Meng Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Junfeng Tian
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hong Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Junfeng Tian .

Editor information

Editors and Affiliations

  1. School of Computer Engineering and Science, Shanghai University, Shanghai, China

    Huaikou Miao

  2. Institute of Computing Theory and Technology, Xidian University, Xi'an, China

    Cong Tian

  3. Hosei University, Tokyo, Japan

    Shaoying Liu

  4. Xidian University, Xi'an, Shaanxi, China

    Zhenhua Duan

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Wang, M., Tian, J., Zhang, H. (2020). UMC4M: A Verification Tool via Program Execution. In: Miao, H., Tian, C., Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2019. Lecture Notes in Computer Science(), vol 12028. Springer, Cham. https://doi.org/10.1007/978-3-030-41418-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-41418-4_7

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation