Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 8

Proceedings of the 2016 Federated Conference on Computer Science and Information Systems

Alvis models of safety critical systems state-base verification with nuXmv

DOI: http://dx.doi.org/10.15439/2016F264

Citation: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, pages 1701–1708 ()

Full text

Abstract. For modelling of real-time safety critical systems, when traditional testing techniques cannot be applied, formal system verification is crucial. Alvis is a modelling language that combines possibilities of formal models verification with flexibility and simplicity of practical programming languages. Solutions introduced in Alvis make the development process easier and help engineers to cope with more complex systems. The paper deals with a state-base approach to the verification of Alvis models. Until the research presented in the paper were conducted, the verification process was mostly action-based. The nuXmv tool, as one of the top model checkers, was selected for the task of state-base verification of Alvis models translated into the SMV modelling language. Paper presents a translation algorithm and usability studies performed on existing safety critical systems.

References

  1. M. Szpyrka, P. Matyasik, and R. Mrówka, “Alvis – modelling language for concurrent systems,” in Intelligent Decision Systems in Large-Scale Distributed Environments, ser. Studies in Computational Intelligence, P. Bouvry, H. Gonzalez-Velez, and J. Kołodziej, Eds. Springer-Verlag, 2011, vol. 362, ch. 15, pp. 315–341.
  2. M. Szpyrka, P. Matyasik, R. Mrówka, and L. Kotulski, “Formal description of Alvis language with α0 system layer,” Fundamenta Informaticae, vol. 129, no. 1-2, pp. 161–176, 2014. http://dx.doi.org/10.3233/FI-2014-967
  3. K. Jensen and L. Kristensen, Coloured Petri nets. Modelling and Validation of Concurrent Systems. Heidelberg: Springer, 2009.
  4. T. Murata, “Petri nets: Properties, analysis and applications,” Proceedings of the IEEE, vol. 77, no. 4, pp. 541–580, 1989.
  5. J. Bengtsson and W. Yi, “Timed automata: Semantics, algorithms and tools,” Lecture Notes on Concurrency and Petri Nets, vol. 3098, 2004.
  6. R. Alur and D. Dill, “A theory of timed automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183–235, 1994.
  7. J. A. Bergstra, A. Ponse, and S. A. Smolka, Eds., Handbook of Process Algebra. Upper Saddle River, NJ, USA: Elsevier Science, 2001.
  8. R. Milner, Communication and Concurrency. Prentice-Hall, 1989.
  9. T. Bolognesi and E. Brinksma, “Introduction to the iso specification language lotos,” Comput. Netw. ISDN Syst., vol. 14, no. 1, pp. 25–59, Mar. 1987. http://dx.doi.org/10.1016/0169-7552(87)90085-7.
  10. C. Baier and J.-P. Katoen, Principles of Model Checking. London, UK: The MIT Press, 2008.
  11. I. Grobelna, R. Wisniewski, M. Grobelny, and M. Wisniewska, “Design and verification of real-life processes with application of petri nets,” IEEE Transactions on Systems, Man, and Cybernetics: Systems, vol. PP, no. 99, pp. 1–14, 2016. http://dx.doi.org/10.1109/TSMC.2016.2531673
  12. P. Matyasik, “Alvis virtual machine,” in Computer Science and Infor- mation Systems (FedCSIS), 2014 Federated Conference on, Sept 2014. http://dx.doi.org/10.15439/2014F267 pp. 1639–1645.
  13. P. Matyasik, M. Szpyrka, and M. Wypych, “Generation of Java code from Alvis model,” in International Conference of Computational Meth- ods in Sciences and Engineering (ICCMSE 2015), ser. AIP Conference Proceedings, vol. 1702. Athens, Greece: AIP Publishing, March 20-23 2015. http://dx.doi.org/10.1063/1.4938890 pp. 100 013–1–100 013–4.
  14. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuXmv symbolic model checker,” in Computer Aided Verification, ser. Lecture Notes in Computer Science, vol. 8559. Springer, 2014, pp. 334–342.
  15. A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, “NUSMV: a new symbolic model checker,” International Journal on Software Tools for Technology Transfer, vol. 2, no. 4, pp. 410–425, 2000.
  16. E. Clarke, O. Grumberg, and D. Peled, Model Checking. Cambridge, Massachusetts: The MIT Press, 1999.
  17. E. Emerson, “Temporal and modal logic,” in Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Elsevier Science, 1990, vol. B, pp. 995–1072.
  18. M. Szpyrka and P. Matyasik, “Formal modelling and verification of concurrent systems with XCCS,” in Proceedings of the 7th International Symposium on Parallel and Distributed Computing (ISPDC 2008), Krakow, Poland, July 1-5 2008, pp. 454–458.
  19. A. Burns and A. Wellings, Concurrent and real-time programming in Ada 2005. Cambridge University Press, 2007.
  20. B. O’Sullivan, J. Goerzen, and D. Stewart, Real World Haskell. Sebastopol, CA, USA: O’Reilly Media, 2008.
  21. M. Szpyrka, P. Matyasik, J. Biernacki, A. Biernacka, M. Wypych, and L. Kotulski, “Hierarchical communication diagrams,” Computing and Informatics, vol. 35, pp. 55–83, 2016.
  22. M. Wypych, M. Szpyrka, and P. Matyasik, “Extension of Alvis compiler front-end,” in International Conference of Computational Methods in Sciences and Engineering (ICCMSE 2015), ser. AIP Conference Proceedings, vol. 1702. Athens, Greece: AIP Publishing, March 20-23 2015. http://dx.doi.org/10.1063/1.4938892 pp. 100 015–1–100 015–4.
  23. M. Szpyrka, P. Matyasik, and M. Wypych, “Generation of labelled transition systems for alvis models using haskell model representation,” in Proceedings of the 22nd International Workshop on Concurrency, Specification and Programming (CS&P 2013), vol. 1032. Warsaw, Poland: CEUR Workshop Proceedings, 2013, pp. 409–420.
  24. E. A. Emerson, “Model checking and the Mu-calculus,” in Descriptive Complexity and Finite Models, ser. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, N. Immerman and P. G. Kolaitis, Eds. American Mathematical Society, 1997, vol. 31, pp. 185–214.
  25. H. Garavel, F. Lang, R. Mateescu, and W. Serwe, “CADP 2006: A toolbox for the construction and analysis of distributed processes,” in Computer Aided Verification (CAV’2007), ser. LNCS, vol. 4590. Berlin, Germany: Springer, 2007, pp. 158–163.
  26. S. Kripke, “A semantical analysis of modal logic I: normal modal propo- sitional calculi,” Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 9, pp. 67–96, 1963, announced in Journal of Symbolic Logic, 24, 1959, p. 323.
  27. ZUE S.A. (2015) Infrared-systems. Http://www.grupazue.pl/en/oferta/produkcja-urzadzen/infrared-systems.
  28. M. Gorowski. (2014) Rail transport. Http://www.transportszynowy.pl/zwrotnicetramsterowanie.php.
  29. J. Ciszewski, K. Kunecki, W. Markowski, J. Sawicki, and M. Sobecki, SITP Guideline WP-02:2010. Fire alarm systems. The design, 2010.
  30. J. Biernacki, A. Biernacka, and M. Szpyrka, “Action-based verification of RTCP-nets with CADP,” in International Conference of Computa- tional Methods in Sciences and Engineering (ICCMSE 2015), ser. AIP Conference Proceedings, vol. 1702. Athens, Greece: AIP Publishing, March 20-23 2015. http://dx.doi.org/10.1063/1.4938888 pp. 100 011–1–100 011–4.