Formal Description of Alvis Language with α⁰ System Layer

• Autorzy: Szpyrka M. , Matyasik P. , Mrówka R. , Kotulski L.

Identyfikatory

DOI

10.3233/FI-2014-967

• Języki publikacji: EN

Abstrakty

EN

The paper presents a formal description of a subset of the Alvis language designed for the modelling and formal verification of concurrent systems. Alvis combines possibilities of a formal models verification with flexibility and simplicity of practical programming languages. Alvis provides a graphical modelling of interconnections among agents and a high level programming language used for the description of agents behaviour. Its semantic depends on the so-called system layer. The most universal system layer α⁰, described in the paper, makes Alvis similar to other formal languages like Petri nets, process algebras, time automata, etc.

Słowa kluczowe

EN

Alvis modelling language; concurrent systems; formal methods

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 129, nr 1/2
• Strony: 161--171
• Opis fizyczny: Bibliogr. 21 poz., rys., tab.

Twórcy

autor

Szpyrka M.

• 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

Mrówka R.

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

autor

Kotulski L.

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

Bibliografia

• [1] Aceto, L., Ingófsdóttir, A., Larsen, K., Srba, J.: Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, Cambridge, UK, 2007.
• [2] Alur, R., Dill, D.: A theory of timed automata, Theoretical Computer Science, 126(2), 1994, 183–235.
• [3] Baier, C., Katoen, J.-P.: Principles of Model Checking, The MIT Press, London, UK, 2008.
• [4] Balicki, K., Szpyrka, M.: Formal Definition of XCCS Modelling Language, Fundamenta Informaticae, 93(1-3), 2009, 1–15.
• [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] Cheng, A. M. K.: Real-time Systems. Scheduling, Analysis, and Verification, Wiley Interscience, New Jersey, 2002.
• [8] Emerson, E. A.: Model checking and the Mu-calculus, in: Descriptive Complexity and Finite Models (N. Immerman, P. G. Kolaitis, Eds.), vol. 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997, 185–214.
• [9] Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes, Computer Aided Verification, 4590, Springer-Verlag, 2007.
• [10] Gnesi, S., Margaria, T., Eds.: Formal Methods for Industrial Critical Systems. A Survey of Applications, John Wiley & Sons, Hoboken, New Jersey, 2013.
• [11] Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, vol. 1–3, Springer-Verlag, Berlin, Germany, 1992-97.
• [12] Kotulski, L., Szpyrka, M., Sędziwy, A.: Labelled Transition System Generation from Alvis Language, in: Knowledge-Based and Intelligent Information and Engineering Systems – KES 2011, vol. 6881 of LNCS, Springer-Verlag, 2011, 180–189.
• [13] Milner, R.: Communication and Concurrency, Prentice-Hall, 1989.
• [14] Murata, T.: Petri Nets: Properties, Analysis and Applications, Proc. of the IEEE, 77(4), 1989, 541–580.
• [15] O’Sullivan, B., Goerzen, J., Stewart, D.: Real World Haskell, O’Reilly Media, Sebastopol, CA, USA, 2008.
• [16] Penczek,W., Półrola, A.: Advances in Verification of Time Petri nets and Timed Automata. A Temporal Logic Approach, vol. 20 of Studies in Computational Intelligence, Springer-Verlag, 2006.
• [17] Suraj, Z., Fryc, B.: Timed approximate Petri nets, Fundamenta Informaticae, 71(1), 2006, 83–99.
• [18] Szpyrka, M.: Analysis of RTCP-nets with Reachability Graphs, Fundamenta Informaticae, 74(2–3), 2006, 375–390.
• [19] Szpyrka, M., Balicki, K.: XCCS – graphical extension of CCS language, Proc. of Mixdes 2007, the 14th Int. Conference Mixed Design of Integrated Circuits and Systems, Ciechocinek, Poland, June 21-23 2007.
• [20] Szpyrka, M., Matyasik, P.: Formal modelling and verification of concurrent systems with XCCS, Proc. of the 7th Int. Symposium on Parallel and Distributed Computing (ISPDC 2008), Krakow, Poland, July 1-5 2008.
• [21] Szpyrka, M., Matyasik, P., Mrówka, R.: Alvis – modelling language for concurrent systems, in: Intelligent Decision Systems in Large-Scale Distributed Environments, vol. 362 of SCI, Springer-Verlag, 2011, 315–342