PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Model checking processes specified in join-calculus algebra

Treść / Zawartość
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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 a chemical abstract machine, serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, allowing for the examination of more complex systems. The described model checker is a proof of concept for the utilization of new methodologies of formal system specification and verification in software engineering practice.
Wydawca
Czasopismo
Rocznik
Strony
61--74
Opis fizyczny
Bibliogr. 16 poz., rys., wykr.
Twórcy
  • AGH University of Science and Technology, Krakow, Poland
  • AGH University of Science and Technology, Krakow, Poland
Bibliografia
  • [1] Aaby A.A.: Compiler Construction using Flex and Bison. Walla Walla College, 2003.
  • [2] Baier C., Katoen J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. ISBN 026202649X, 9780262026499.
  • [3] Ben-Ari M.: Mathematical Logic for Computer Science. Prentice-Hall International Series in Computer Science. Springer, 2001. ISBN 9781852333195, URLhttp://books.google.pl/books?id=hzWlEy1qqR8C.
  • [4] 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.
  • [5] 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. URLhttp://dx.doi.org/http://doi.acm.org/10.1145/96709.96717.
  • [6] 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.
  • [7] 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.
  • [8] Edmund M., Clarke J., Grumberg O., Peled D.A.: Model Checking. MIT Press, Cambridge, MA, USA, 1999. ISBN 0-262-03270-8.
  • [9] 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.
  • [10] 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.
  • [11] 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.
  • [12] Grumberg O., Veith H., eds.:25 Years of Model Checking – History, Achievements, Perspectives, Lecture Notes in Computer Science, vol. 5000. Model checking processes specified in join-calculus algebra 73 Springer, 2008. ISBN 978-3-540-69849-4.
  • [13] Herlihy M., Shavit N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2008. ISBN 0123705916, 9780123705914.
  • [14] Holzmann G.: SPIN Model Checker, Primer and Reference Manual. 1st. ed. Addison-Wesley Professional, 2003. ISBN 0-321-22862-6.
  • [15] Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J.: Symbolic Model Checking: 1020 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.
  • [16] 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
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-6f50b280-a521-4827-829e-94c0314dcd15
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.