Warianty tytułu
Języki publikacji
Abstrakty
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 α0, described in the paper, makes Alvis similar to other formal languages like Petri nets, process algebras, time automata, etc.
Słowa kluczowe
Czasopismo
Rocznik
Tom
Strony
161--171
Opis fizyczny
Bibliogr. 21 poz., rys., tab.
Twórcy
autor
- AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland, mszpyrka@agh.edu.pl
autor
- AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland, ptm@agh.edu.pl
autor
- AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland, Rafal.Mrowka@agh.edu.pl
autor
- AGH University of Science and Technology, Department of Applied Computer Science, Al. Mickiewicza 30, 30-059 Krakow, Poland, kotulski@agh.edu.pl
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
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.baztech-954efd9e-7ef4-4ed4-96c0-7544eae48ed4