Abstract
Like reachability, coverability is an important tool for verifying behavioural properties of dynamic systems. When a system is modelled as a Petri net, the classical Karp-Miller coverability tree construction can be used to decide questions related to the (required) capacity of local states. Correctness (termination) of the construction is based on a monotonicity property: more resources available implies more behaviour possible. Here we discuss a modification of the coverability tree construction allowing one to deal with concurrent occurrences of actions (steps) and to extend the notion of coverability to a dynamic action-based notion (thus viewing bandwidth as a resource). We are in particular interested in component-based systems in which steps are subject to additional constraints like (local) synchronicity or maximal concurrency. In general the behaviour of such systems is not monotonous and hence new termination criteria (depending on the step semantics) are needed. We here investigate marked graphs, a Petri net model for systems consisting of concurrent components communicating via buffers.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agerwala, T.: A Complete Model for Representing the Coordination of Asynchronous Processes. In: Hopkins Comp. Research Rep., vol. 32. Johns Hopkins Univ. (1974)
Baeten, J.C.M., Weijland, W.P.: Process algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)
Busi, N.: Analysis Issues in Petri Nets with Inhibitor Arcs. Theoretical Computer Science 275, 127–177 (2002)
Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked Directed Graphs. J. Comput. Syst. Sci. 5, 511–523 (1971)
Darondeau, P., Genest, B., Thiagarajan, P.S., Yang, S.: Quasi-Static Scheduling of Communicating Tasks. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 310–324. Springer, Heidelberg (2008)
Desel, J., Esparza, J.: Free Choice Nets. Cambridge University Press, Cambridge (1995)
Desel, J., Reisig, W.: Place/Transition Petri Nets. In: [20], pp. 122–173
Esparza, J., Nielsen, M.: Decidability Issues for Petri Nets: A Survey. J. of Inf. Processing and Cybernetics 30, 143–160 (1994)
Ghamarian, A.H., Geilen, M.C.W., Basten, T., Theelen, B.D., Mousavi, M.R., Stuijk, S.: Liveness and Boundedness of Synchronous Data Flow Graphs. In: FMCAD 2006, pp. 12–16 (2006)
Hack, M.: Decision Problems for Petri Nets and Vector Addition Systems. Technical Memo 59, Project MAC, MIT (1975)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Karp, R.M., Miller, R.E.: Parallel Program Schemata. J. Comput. Syst. Sci. 3, 147–195 (1969)
Kleijn, J., Koutny, M.: Steps and Coverability in Inhibitor Nets. In: Lodaya, K., Mukund, M., Ramanujam, R. (eds.) Perspectives in Concurrency Theory, pp. 264–295. Universities Press, Hyderabad (2008)
Kleijn, J., Koutny, M., Rozenberg, G.: Process Semantics for Membrane Systems. J. of Aut., Lang. and Comb. 11, 321–340 (2006)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes. Inf. and Comp. 100, 1–77 (1992)
Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice-Hall, Englewood Cliffs (1981)
Petri, C.A.: Fundamentals of a Theory of Asynchronous Information Flow. In: IFIP Congress 1962, pp. 386–390. North Holland, Amsterdam (1962)
Rozenberg, G., Engelfriet, J.: Elementary Net Systems. In: [20], 12–121
Reisig, W., Rozenberg, G. (eds.): APN 1998. LNCS, vol. 1491. Springer, Heidelberg (1998)
Rozenberg, G., Thiagarajan, P.S.: Petri Nets: Basic Notions, Structure, Behaviour. In: Rozenberg, G., de Bakker, J.W., de Roever, W.-P. (eds.) Current Trends in Concurrency. LNCS, vol. 224, pp. 585–668. Springer, Heidelberg (1986)
Valmari, A.: The State Explosion Problem. In: [20], 429–528
Wimmel, H.: Entscheidbarkeitsfragen bei Petri Netzen. Habilitation (2007)
Yoeli, M.: Specification and Verification of Asynchronous Circuits using Marked Graphs. In: Rozenberg, G. (ed.) APN 1987. LNCS, vol. 266, pp. 605–622. Springer, Heidelberg (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kleijn, J., Koutny, M. (2010). Applying Step Coverability Trees to Communicating Component-Based Systems . In: Arbab, F., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2009. Lecture Notes in Computer Science, vol 5961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11623-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-11623-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11622-3
Online ISBN: 978-3-642-11623-0
eBook Packages: Computer ScienceComputer Science (R0)