Communication with Environment in Alvis Models

• Autorzy: Szpyrka M. , Matyasik P. , Mrówka R. , Kotulski L.
• Języki publikacji: EN

Abstrakty

EN

Alvis is a modelling language defined for the design and a formal verification of embedded systems. An Alvis model is a system of agents that usually run concurrently, communicate one with another, compete for shared resources etc. Due to the fact that an embedded system usually collects inputs that come from its environment and provides outputs that go to the environment it is necessary to provide a mechanism to describe such a communication. In contrast to another formal languages used to model embedded systems it is not necessary, using Alvis, to design such an environment as a part of a model. The paper deals with the problem of modelling a communication with an embedded system environment with Alvis.

Słowa kluczowe

EN

Alvis modelling language; embedded system; formal verification; communication with environment

• Wydawca: Polish Academy of Sciences, Committee of Electronics and Telecommunication
• Czasopismo: International Journal of Electronics and Telecommunications
• Rocznik: 2012
• Tom: Vol. 58, No. 3
• Strony: 247--254
• Opis fizyczny: Bibliogr. 16 poz., wykr.

Twórcy

autor

Szpyrka M.

autor

Matyasik P.

autor

Mrówka R.

autor

Kotulski L.

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

Bibliografia

• [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. SCI. Springer-Verlag, 2011, vol. 362, pp. 315-342.
• [2] M. Szpyrka, Alvis On-line Manual, AGH UST, Krakow, Poland, 2012. [Online]. Available: http://fm.ia.agh.edu.pl/alvis:manual
• [3] T. Murata, “Petri nets: Properties, analysis and applications,” Proceedings of the IEEE, vol. 77, no. 4, pp. 541-580, 1989.
• [4] K. Jensen and L. Kristensen, Coloured Petri nets. Modelling and Validation of Concurrent Systems. Heidelberg: Springer, 2009.
• [5] M. Szpyrka and T. Szmuc, “Verification of automatic train protection systems with RTCP-nets,” in Computer Safety, Reliability and Security, ser. LNCS, J. Górski, Ed. Springer-Verlag, 2006, vol. 4166, pp. 344-357.
• [6] J. A. Bergstra, A. Ponse, and S. A. Smolka, Eds., Handbook of Process Algebra. Upper Saddle River, NJ, USA: Elsevier Science, 2001.
• [7] L. Aceto, A. Ingófsdóttir, K. Larsen, and J. Srba, Reactive Systems: Modelling, Specification and Verification. Cambridge, UK: Cambridge University Press, 2007.
• [8] 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, ser. LNCS, vol. 4590. Springer-Verlag, 2007, pp. 158-163.
• [9] K. Balicki and M. Szpyrka, “Formal definition of XCCS modelling language,” Fundamenta Informaticae, vol. 93, no. 1-3, pp. 1-15, 2009.
• [10] P. Matyasik, “Design and analysis of embedded systems with XCCS process algebra,” Ph.D. dissertation, AGH University of Science and Technology, Kraków, Poland, 2009.
• [11] R. Milner, Communication and Concurrency. Prentice-Hall, 1989.
• [12] B. O’Sullivan, J. Goerzen, and D. Stewart, Real World Haskell. Sebastopol, CA, USA: O’Reilly Media, 2008.
• [13] J. Barnes, Programming in Ada 2005. Addison Wesley, 2006.
• [14] M. Szpyrka, L. Kotulski, and P. Matyasik, “Specification of embedded systems environment behaviour with Alvis modelling language,” in Proc. of the 2011 Int. Conf. on Embedded Systems and Applications ESA’11 (Worldcomp 2011), Las Vegas, Nevada, USA, July 18-21 2011, pp. 79-85.
• [15] M. Szpyrka, P. Matyasik, R. Mrówka, and L. Kotulski, “Formal modelling and verification of concurrent systems with Alvis,” International Journal of Applied Mathematics and Computer Science, 2012, (to appear).
• [16] L. Kotulski, M. Szpyrka, and A. Sędziwy, “Labelled transition system generation from Alvis language,” in Knowledge-Based and Intelligent Information and Engineering Systems - KES 2011, ser. LNCS. Springer-Verlag, 2011, vol. 6881, pp. 180-189.