Skip to main content
SpringerLink
Log in

Extending MSVL with Semaphore

  • Conference paper
  • First Online:
Computing and Combinatorics (COCOON 2016)

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

Included in the following conference series:

Abstract

Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easy to use, we extend MSVL with the technique of semaphore. To do so, the mechanism of MSVL function calls is deeply analyzed. Further, the semaphore type is defined. Moreover, operations over semaphore are formalized. Finally, an example is given to illustrate how to use semaphore to solve the mutual exclusion problem.

This research is supported by Natural Science Foundation of Education Bureau of Shaanxi Province (No. 11JK1037), NSFC Grant Nos. 61133001, 61420106004, 91418201 and 61322202.

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. Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  4. Wang, M., Duan, Z., Tian, C.: Simulation and verification of the virtual memory management system with MSVL. In: Proceedings of the 2014 IEEE 18th International Conference on Computer Supported Cooperative Work in Design (CSCWD), pp. 360–365, May 2014

    Google Scholar 

  5. Yu, Y., Duan, Z., Tian, C., Yang, M.: Model checking C programs with MSVL. In: Liu, S. (ed.) SOFL 2012. LNCS, vol. 7787, pp. 87–103. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Ma, Q., Duan, Z., Zhang, N., Wang, X.: Verification of distributed systems with the axiomatic system of MSVL. Formal Asp. Comput. 27(1), 103–131 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  7. Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729–1744 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  8. Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167–186. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Milner, R.: Communication and Concurrency. Prentice Hall, London (1989)

    MATH  Google Scholar 

  10. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, London (1985)

    MATH  Google Scholar 

  11. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  12. Dijkstra, E.W.: Over de sequentialiteit van procesbeschrijvingen (EWD-35). E.W. Dijkstra Archive. Center for American History, University of Texas at Austin

    Google Scholar 

  13. Zhang, N., Duan, Z., Tian, C.: Extending MSVL with function calls. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 446–458. Springer, Heidelberg (2014)

    Google Scholar 

  14. Arpaci-Dusseau, R.H.: Operating Systems: Three Easy Pieces [Chapter: Condition Variables]. Arpaci-Dusseau Books (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Technology, Xi’an University of Posts and Communications, Xi’an, 710061, China

    Xinfeng Shu

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

    Zhenhua Duan

Authors
  1. Xinfeng Shu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhenhua Duan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhenhua Duan .

Editor information

Editors and Affiliations

  1. Virginia Commonwealth Univ , Richmond, Virginia, USA

    Thang N. Dinh

  2. University of Florida , Gainesville, Alabama, USA

    My T. Thai

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Shu, X., Duan, Z. (2016). Extending MSVL with Semaphore. In: Dinh, T., Thai, M. (eds) Computing and Combinatorics . COCOON 2016. Lecture Notes in Computer Science(), vol 9797. Springer, Cham. https://doi.org/10.1007/978-3-319-42634-1_48

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-42634-1_48

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-42633-4

  • Online ISBN: 978-3-319-42634-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation