×

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].

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.)

Software:

SPIN
PDFBibTeX XMLCite
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.