Introduction to modelling embedded systems with Alvis

• Autorzy: Szpyrka M. , Matyasik P. , Mrówka R. , Witalec W. , Baniewicz J. , Kotulski L.

Warianty tytułu

PL

Wprowadzenie do modelowania systemów wbudowanych w języku Alvis

• Języki publikacji: EN

Abstrakty

EN

Alvis is a modelling language for concurrent and real-time systems. It combines hierarchical graphical modelling with a Haskell-based high level programming language. The graphical layer is used to define data and control flow among agents. The code layer is used to describe the behaviour of individual agents. An Alvis model is transformed into a labelled transition system (LTS) that is used for formal verification of the model. The paper discusses some aspects of modelling embedded systems with Alvis.

PL

Alvis jest językiem modelowania rozwijanym z myślą o systemach współbieżnych w szczególności systemach wbudowanych. Łączy on w sobie graficzny język modelowania, przeznaczony do definiowania połączeń komunikacyjnych między agentami, z językiem programowania wysokiego poziomu, przeznaczonym do definiowania zachowania poszczególnych agentów. W artykule przedstawiono wybrane aspekty modelowania systemów wbudowanych z użyciem języka Alvis.

Słowa kluczowe

EN

Alvis; embedded systems modelling; veryfication systems modelling; formal methods

PL

Alvis; modelowanie systemów wbudowanych; weryfikacja systemów wbudowanych; metody formalne

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
• Rocznik: 2011
• Tom: T. 15, z. 2
• Strony: 435--442
• Opis fizyczny: Bibliogr. 18 poz., rys., tab.

Twórcy

autor

Szpyrka M.

• AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, IT and Electronics, Department of Automatics

autor

Matyasik P.

• AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, IT and Electronics, Department of Automatics

autor

Mrówka R.

• AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, IT and Electronics, Department of Automatics

autor

Witalec W.

• AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, IT and Electronics, Department of Automatics

autor

Baniewicz J.

• Electronic Controls/E&S, Delphi Poland S.A., Kraków

autor

Kotulski L.

• AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, IT and Electronics, Department of Automatics

Bibliografia

• [1] Aceto L., Ingófsdóttir A., Larsen K.G., Srba J., Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge, UK, 2007.
• [2] Alur R., Diii D., A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
• [3] Balicki K., Szpyrka M., Formal definition of XCCS modelling language. Fundamenta Informaticae, 93(1-3): 1-15, 2009.
• [4] Barnes J., Programming in Ada 2005. Addison Wesley, 2006.
• [5] Bengtsson J., Yi W., Timed automata: Semantics, algorithms and tools. Lecture Notes on Concurrency and Petri Nets, 3098, 2004.
• [6] Bergstra J.A., Ponse A., Smolka S.A. (Eds). Handbook of Process Algebra. Elsevier Science, Upper Saddle River, NJ, USA, 2001.
• [7] Garavel H., Lang R, Mateescu R., Serwe W., CADP 2006: A toolbox for the construction and analysis of distributed processes. In Computer Aided Verification (CAV'2OO7), volume 4590 of LNCS, pages 158-163, Berlin, Germany, 2007. Springer.
• [8] Hoare C.A.R., Communicating seąuentialprocesses. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985.
• [9] Jensen K., ColouredPetri Nets. Basic Concepts, Analysis Methods andPractical Use. volume 1-3. Springer-Verlag, Berlin, Germany, 1992-97.
• [10] Jensen K., Kristensen L.M., Coloured Petri nets. Modelling and Yalidation of Concurrent Systems. Springer, Heidelberg, 2009.
• [11] Matyasik R, Design and analysis of embedded systems with XCCSprocess algebra. PhD thesis, AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, Computer Science and Electronics, Kraków, Poland, 2009.
• [12] Milner R., Communication and Concurrency. Prentice-Hall, 1989.
• [13] Murata T., Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-580, 1989.
• [14] O'Sullivan B., Goerzen J., Stewart D., Real World Haskell. 0'Reilly Media, Sebastopol, CA, USA, 2008.
• [15] Szpyrka M., Petri nets for modelling and analysis of concurrent systems. WNT, Warsaw 2008 (in Polish).
• [16] Szpyrka M., Alvis On-line Manuał. AGH University of Science and Technology, 2011.
• [17] Szpyrka M., Kotulski L., Matyasik P., Specification of embedded systems environment behaviour with Alvis modelling language. In Proc. of the 2011 International Conference on Embedded Systems and Applica-tions ESA'll (part of Worldcomp 2011), Las Vegas, Nevada, USA, 2011.
• [18] Szpyrka M., Matyasik R, Mrówka R., Alvis - modelling language for concurrent systems. In P. Bouvry, Gonzalez-Velez H., Kołodziej J. (Eds), Intelligent Decision Systems in Large-Scale Distributed Emdronments, Studies in Computational Intelligence, vol. 362, Springer-Verlag, 2011, 315-342.