Shu, Xinfeng; Duan, Zhenhua Extending MSVL with semaphore. (English) Zbl 1476.68183 Dinh, Thang N. (ed.) et al., Computing and combinatorics. 22nd international conference, COCOON 2016, Ho Chi Minh City, Vietnam, August 2–4, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9797, 599-610 (2016). Summary: 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.For the entire collection see [Zbl 1342.68014]. Cited in 2 Documents MSC: 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68N17 Logic programming 68Q60 Specification and verification (program logics, model checking, etc.) Keywords:temporal logic programming; projection; semaphore; mutual exclusion; concurrency Software:SPIN PDFBibTeX XMLCite \textit{X. Shu} and \textit{Z. Duan}, Lect. Notes Comput. Sci. 9797, 599--610 (2016; Zbl 1476.68183) Full Text: DOI References: [1] Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008) · Zbl 1131.68036 · doi:10.1016/j.scico.2007.09.001 [2] Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005) [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) · Zbl 1141.68039 · doi:10.1007/s00236-007-0062-z [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 · doi:10.1109/CSCWD.2014.6846870 [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) · Zbl 06321028 · doi:10.1007/978-3-642-39277-1_7 [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) · Zbl 1328.68032 · doi:10.1007/s00165-014-0303-1 [7] Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729–1744 (2011) · Zbl 1221.03018 · doi:10.1016/j.tcs.2010.12.047 [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) · Zbl 05362215 · doi:10.1007/978-3-540-88194-0_12 [9] Milner, R.: Communication and Concurrency. Prentice Hall, London (1989) · Zbl 0683.68008 [10] Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, London (1985) · Zbl 0637.68007 [11] Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997) · Zbl 05113845 · doi:10.1109/32.588521 [12] Dijkstra, E.W.: Over de sequentialiteit van procesbeschrijvingen (EWD-35). E.W. Dijkstra Archive. Center for American History, University of Texas at Austin [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) · Zbl 06587199 · doi:10.1007/978-3-319-11737-9_29 [14] Arpaci-Dusseau, R.H.: Operating Systems: Three Easy Pieces [Chapter: Condition Variables]. Arpaci-Dusseau Books (2014) This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.