Model checking processes specified in join-calculus algebra

Sławomir Piotr Maludziński; Grzegorz Dobrowolski

doi:10.7494/csci.2014.15.1.61

Authors

Sławomir Piotr Maludziński AGH University of Science and Technology al. Mickiewicza 30, PL-30-059 Kraków
Grzegorz Dobrowolski

DOI:

https://doi.org/10.7494/csci.2014.15.1.61

Keywords:

join-calculus, model checking, formal methods, authomatic software verification

Abstract

This article presents a model checking tool used to verify concurrent systems specified in join-calculus algebra. The temporal properties of systems under verification are expressed in CTL logic. Join-calculus algebra with its operational semantics defined by the chemical abstract machine serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, and allows the examination of more complex systems.

Downloads

Download data is not yet available.

Author Biography

Sławomir Piotr Maludziński, AGH University of Science and Technology al. Mickiewicza 30, PL-30-059 Kraków

AGH University of Science and Technology
al. Mickiewicza 30, PL-30-059 Kraków

References

Aaby A. A.: Compiler Construction using Flex and Bison. Walla Walla College, 2003.

Baier C., Katoen J. P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. ISBN 026202649X, 9780262026499.

Ben-Ari M.: Mathematical Logic for Computer Science. Prentice-Hall International Series in Computer Science. Springer, 2001. ISBN 9781852333195, URL http://books.google.pl/books?id=hzWlEy1qqR8C.

Ben-Ari M., Manna Z., Pnueli A.: The Temporal Logic of Branching Time. In:Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’81, pp. 164–176. ACM, New York, NY, USA, 1981. ISBN 0-89791-029-X. URL http://dx.doi.org/10.1145/567532.567551.

Berry G., Boudol G.: The Chemical Abstract Machine. In: POPL ’90: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81–94. ACM, New York, NY, USA, 1990. ISBN 0-89791-343-4. URL http://dx.doi.org/http://doi.acm.org/10.1145/96709.96717.

Cimatti A., Clarke E., Giunchiglia E., Giunchiglia F., Pistore M., Roveri M., Sebastiani R., Tacchella A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Proc. International Conference on Computer-Aided Verification (CAV 2002), LNCS, vol. 2404. Springer, Copenhagen, Denmark, 2002.

Dennis L. A., Fisher M., Webster M. P., Bordini R. H.: Model Checking Agent Programming Languages. Automated Software Engg., 19(1): 5–63, 2012. ISSN 0928-8910. URL http://dx.doi.org/10.1007/s10515-011-0088-x.

Edmund M., Clarke J., Grumberg O., Peled D. A.: Model Checking. MIT Press, Cambridge, MA, USA, 1999. ISBN 0-262-03270-8.

Ferrari G. L., Montanari U., Tuosto E.: Model Checking for Nominal Calculi. In: Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS’05, pp. 1–24. Springer-Verlag, Berlin, Heidelberg, 2005. ISBN 3-540-25388-2, 978-3-540-25388-4. URL http://dx.doi.org/10.1007/978-3-540-31982-5_1.

Fournet C., Gonthier G.: The Reﬂexive CHAM and the Join-calculus. In: POPL’96: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 372–385. ACM, New York, NY, USA, 1996. ISBN 0-89791-769-3. URL http://dx.doi.org/http://doi.acm.org/10.1145/237721.237805.

Fournet C., Gonthier G., Lévy J. J., Maranget L., Rémy D.: A Calculus of Mobile Agents. In: Proceedings of the 7th International Conference on Concurrency Theory (CONCUR’96), pp. 406–421. Springer-Verlag, 1996. URL citeseer.ist.psu.edu/fournet96calculus.html.

Grumberg O., Veith H., eds.: 25 Years of Model Checking – History, Achievements, Perspectives, Lecture Notes in Computer Science, vol. 5000. Springer, 2008. ISBN 978-3-540-69849-4.

Herlihy M., Shavit N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2008. ISBN 0123705916, 9780123705914.

Holzmann G.: SPIN Model Checker, Primer and Reference Manual. 1 st. ed. Addison-Wesley Professional, 2003. ISBN 0-321-22862-6.

Burch J. R., Clarke E. M., McMillan K. L., Dill D. L., Hwang L. J.: Symbolic Model Checking: 10 20 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1–33. IEEE Computer Society Press, Washington, D.C., 1990. URL citeseer.ist.psu.edu/burch90symbolic.html.

Niewiadomski A., Penczek W., Szreter M.: A Model Checker for Real Time and Multi-agent Systems. In: Proceedings of VerICS 2004, pp. 88–99. Humboldt University, 2004.