A survey of Alvis communication modes

• Autorzy: Szpyrka M. , Biernacki J. , Matyasik P. , Wypych M.
• Języki publikacji: EN

Abstrakty

EN

Concurrent systems appear natural and intuitive solution for many real IT problems. However, designing a more complex concurrent system is a difficult task. The main problem is that for systems that have more than several subsystems it becomes difficult to control their properties at the design stage. Applications of formal methods in the development process may remarkable reduce the problem. An important issue is to choose a suitable formal modelling language, that supports the required methods of communication between subsystems. The paper provides a survey of communication modes introduced to the Alvis modelling language and discusses how the communication modes may be used while modelling concurrent systems.

Słowa kluczowe

EN

Alvis language; communication modes; concurrent systems; real-time systems

PL

język modelowania Alvis; tryby komunikacji; systemy współbieżne; systemy czasu rzeczywistego

• Wydawca: Lodz University of Technology. Department of Microelectronics and Computer Science
• Czasopismo: International Journal of Microelectronics and Computer Science
• Rocznik: 2017
• Tom: Vol. 8, nr 1
• Strony: 1--9
• Opis fizyczny: Bibliogr. 24 poz., il., rys.

Twórcy

autor

Szpyrka M.

• AGH University of Science and Technology, Department of Applied, Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland

autor

Biernacki J.

• AGH University of Science and Technology, Department of Applied, Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland

autor

Matyasik P.

• AGH University of Science and Technology, Department of Applied, Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland

autor

Wypych M.

• AGH University of Science and Technology, Department of Applied, Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland

Bibliografia

• [1] C. Baier and J.-P. Katoen, Principles of Model Checking. London, UK: The MIT Press, 2008.
• [2] I. Grobelna, M. Wiśniewska, R. Wiśniewski, M. Grobelny, and P. Mróz, “Decomposition, validation and documentation of control process specification in form of a Petri net,” in 7th International Conference on Human System Interactions (HSI), Lisbon, Portugal, 2014, pp. 232-237.
• [3] M. Jamro, D. Rzonca, and W. Rząsa, “Testing communication tasks in distributed control systems with SysML and timed colored Petri nets model,” Computers in Industry, vol. 71, pp. 77-87, 2015.
• [4] M. Szpyrka, J. Biernacki, and A. Biernacka, “Tools and methods for RTCP-nets modelling and verification,” Archives of Control Sciences, vol. 26, no. 3, pp. 339-365, 2016.
• [5] R. Milner, Communication and Concurrency. Prentice-Hall, 1989.
• [6] L. Aceto, A. Ingófsdóttir, K. Larsen, and J. Srba, Reactive Systems: Modelling, Specification and Verification. Cambridge, UK: Cambridge University Press, 2007.
• [7] C. A. R. Hoare, Communicating sequential processes. Upper Saddle River, NJ, USA: Prentice-Hall, Inc., 1985.
• [8] J. A. Bergstra, A. Ponse, and S. A. Smolka, Eds., Handbook of Process Algebra. Upper Saddle River, NJ, USA: Elsevier Science, 2001.
• [9] ISO, “Information processing systems, open systems interconnection LOTOS,” Tech. Rep. ISO 8807, 1989.
• [10] N. Maneerat, R. Varakulsiripunth, D. Seki, K. Yoshida, K. Takahashi, Y. Kato, B. Bista, and N. Shiratori, “Composition method of communication system specifications in asynchronous model and its support system,” in Proceedings of 9th IEEE International Conference on Networks, 2001, pp. 64-69.
• [11] J. Bengtsson and W. Yi, “Timed automata: Semantics, algorithms and tools,” Lecture Notes on Concurrency and Petri Nets, vol. 3098, 2004.
• [12] 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.
• [13] 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.
• [14] M. Szpyrka, P. Matyasik, J. Biernacki, A. Biernacka, M. Wypych, and L. Kotulski, “Hierarchical communication diagrams,” Computing and Informatics, vol. 35, no. 1, pp. 55-83, 2016.
• [15] P. Matyasik, M. Szpyrka, M.Wypych, and J. Biernacki, “Communication between agents in Alvis language,” in Proc. of Mixdes 2016, the 23nd International Conference Mixed Design of Integrated Circuits and Systems, Łódź, Poland, June 23-25 2016, pp. 448-453.
• [16] 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.
• [17] A. Burns and A. Wellings, Concurrent and real-time programming in Ada 2005. Cambridge University Press, 2007.
• [18] B. O’Sullivan, J. Goerzen, and D. Stewart, Real World Haskell. Sebastopol, CA, USA: O’Reilly Media, 2008.
• [19] 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.
• [20] 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. LNCS. Springer-Verlag, 2014, vol. 8559, pp. 334-342.
• [21] J. Biernacki, “Alvis models of real-time safety critical systems statebase verification with nuXmv,” in Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), ser. ACSIS, vol. 8, 2016, pp. 1701-1708.
• [22] 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.
• [23] E. Clarke, O. Grumberg, and D. Peled, Model Checking. Cambridge, Massachusetts: The MIT Press, 1999.
• [24] M. Szpyrka, J. Biernacki, A. Biernacka, and M. Wypych, “Priority management in Alvis language,” in Proc. of Mixdes 2016, the 23nd International Conference Mixed Design of Integrated Circuits and Systems, Łódź, Poland, June 23-25 2016, pp. 464-468.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).