Model checking processes specified in join-calculus algebra

Sławomir Piotr Maludziński, Grzegorz Dobrowolski

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.

Keywords


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

Full Text:

PDF

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




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

Refbacks

  • There are currently no refbacks.