×

zbMATH — the first resource for mathematics

Extending MSVL with semaphore. (English) Zbl 06622062
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:
68Rxx Discrete mathematics in relation to computer science
Software:
SPIN
PDF BibTeX XML Cite
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
[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
[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
[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
[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
[7] Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412(18), 1729–1744 (2011) · Zbl 1221.03018
[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
[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
[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
[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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.