Abstract
An embedded system usually consists of a set of sensors cooperating with one or more decisions centres. The design of such a system complicates in respect of both a complicated scheme of components interconnections and their parallel execution. In practice, the latter one excludes testing as a way to guarantee an expected level of a system quality. Thus, a formal verification of such systems is necessary. Alvis is a novel modelling language designed especially for embedded systems. However, it can be used for modelling any information system with concurrent activities. The key concept of Alvis is an agent that denotes any distinguished part of the system under consideration with defined identity persisting in time. The behaviour of agents is defined using Alvis Code Language (AlvisCL) that resembles high level programming languages. Interconnections among agents are defined using Communication Diagrams (AlvisCD) – a visual hierarchical modelling notation. For formal verification purposes, an LTS graph (Labelled Transition System) is generated for an Alvis model. The paper deals with the problem of encoding time relationships with LTS graphs if a model with agents that run concurrently is considered. As a solution, snapshot reachability graphs are proposed.
The paper is supported by the Alvis Project funded from 2009-2010 resources for science as a research project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)
Jensen, K.: Coloured Petri Nets. In: Basic Concepts, Analysis Methods and Practical Use, vol. 1-3. Springer, Heidelberg (1992)
Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Szpyrka, M.: Analysis of RTCP-nets with reachability graphs. Fundamenta Informaticae 74(2-3), 375–390 (2006)
Samolej, S., Rak, T.: Simulation and performance analysis of distributed internet systems using TCPNs. Informatica (Slovenia) 33(4), 405–415 (2009)
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier Science, Upper Saddle River (2001)
Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall, Inc., Upper Saddle River (1985)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Aceto, L., Ingófsdóttir, A., Larsen, K., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Szpyrka, M., Matyasik, P., Mrówka, R.: Alvis – modelling language for concurrent systems. In: Bouvry, P., González-Vélez, H., Kołodziej, J. (eds.) Intelligent Decision Systems in Large-Scale Distributed Environments. SCI, vol. 362, pp. 315–341. Springer, Heidelberg (2011)
Balicki, K., Szpyrka, M.: Formal definition of XCCS modelling language. Fundamenta Informaticae 93(1-3), 1–15 (2009)
Matyasik, P.: Design and analysis of embedded systems with XCCS process algebra. PhD thesis, AGH University of Science and Technology, Faculty of Electrical Engineering, Automatics, Computer Science and Electronics, Kraków, Poland (2009)
Barnes, J.: Programming in Ada 2005. Addison Wesley, Reading (2006)
ISO: Information processing systems, open systems interconnection LOTOS. Technical Report ISO 8807 (1989)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Object Management Group: OMG Systems Modeling Language (OMG Sys ML) (2008)
Ashenden, P.: The Designer’s Guide to VHDL, 3rd edn., vol. 3. Morgan Kaufmann, San Francisco (2008)
Berry, G.: The Esterel v5 Language Primer Version v5 91. Centre de Mathématiques Appliquées Ecole des Mines and INRIA (2000)
Palshikar, G.: An introduction to Esterel. Embedded Systems Programming 14(11) (2001)
Esterel Technologies SA: Welcome to SCADE 6.0. (2007)
Szpyrka, M.: Alvis On-line Manual. AGH University of Science and Technology (2011), http://fm.ia.agh.edu.pl/alvis:manual
O’Sullivan, B., Goerzen, J., Stewart, D.: Real World Haskell. O’Reilly Media, Sebastopol (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Szpyrka, M., Kotulski, L. (2011). Snapshot Reachability Graphs for Alvis Models. In: König, A., Dengel, A., Hinkelmann, K., Kise, K., Howlett, R.J., Jain, L.C. (eds) Knowledge-Based and Intelligent Information and Engineering Systems. KES 2011. Lecture Notes in Computer Science(), vol 6881. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23851-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-23851-2_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23850-5
Online ISBN: 978-3-642-23851-2
eBook Packages: Computer ScienceComputer Science (R0)