Abstract
Scenario-based specifications such as message sequence charts (MSCs) offer an intuitive and visual way of describing design requirements. As one powerful formalism, Petri nets can model concurrency constraints in a natural way, and are often used in modelling system specifications and designs. Since there are gaps between MSC models and Petri net models, keeping consistency between these two kinds of models is important for the success of software development. In this paper, we use Petri nets to model concurrent systems, and consider the problem of checking Petri nets for scenario-based specifications expressed by message sequence charts. We develop the algorithms to solve the following two verification problems: the existential consistency checking problem, which means that a scenario described by a given MSC must happen during a Petri net runs, or any forbidden scenario described by a given MSC never happens during a Petri net run; and the mandatory consistency checking problem, which means that if a reference scenario described by the given MSCs occurs during a Petri net run, it must adhere to a scenario described by the other given MSC.
Supported by the National Natural Science Foundation of China (No.60425204, No.60233020, and No.60273036), the National Grand Fundamental Research 973 Program of China (No.2002CB312001), and by Jiangsu Province Research Foundation (No.BK2004080, No.BK2003408)
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
ITU-T. Recommendation Z.120. ITU - Telecommunication Standardization Sector, Geneva, Switzerland (May 1996)
Peterson, J.L.: Petri Nets Theory and the Modeling of Systems. Prentice-Hall, N.J (1981)
Kluge, O.: Modelling a Railway Crossing with Message Sequence Charts and Petri Nets. In: Ehrig, H., Reisig, W., Rozenberg, G., Weber, H. (eds.) Petri Net Technology for Communication-Based Systems. LNCS, vol. 2472, pp. 197–218. Springer, Heidelberg (2003)
van der Aalst, W.M.P.: Interorganizational Workflows: An Approach based on Message Sequence Charts and Petri Nets. Systems Analysis - Modelling - Simulation 34(3), 335–367 (1999)
Rueppel, U., Meissner, U.F., Greb, S.: A Petri Net based Method for Distributed Process Modelling in Structural Engineering. In: Proc. International Conference on Computing in Civil and Building Engineering (2004)
Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Comparing Different Approaches for Specifying and Verifying Real-Time Systems. In: Proc. 10th IEEE Workshop on Real-Time Operating Systems and Software, New York, pp. 122–129 (1993)
Peled, D.A.: Software Reliability Methods. Springer, Heidelberg (2001)
Alur, R., Holzmann, G.J., Peled, D.: An Analyzer for Message Sequence Charts. Software-Concepts and Tools 17, 70–77 (1996)
Ladkin, P.B., Leue, S.: Interpreting Message Flow Graphs. Formal Aspects of Computing 7(5), 473–509 (1995)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1999)
Bernardi, S., Donatelli, S., Merseguer, J.: From UML sequence diagrams and statecharts to analysable petri net models. In: Proceedings of the third international workshop on Software and performance, pp. 35–45. ACM Press, New York (2002)
Schafer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Electronic Notes in Theoretical Computer Science, vol. 55(3) (2001)
Holzmann, G.J.: The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)
Bontemps, Y., Heymans, P.: Turning High-Level Live Sequence Charts into Automata. In: Proceedings of Workshop: Scenarios and State-Machines (2002)
Berthomieu, B., Diaz, M.: Modelling and verification of time dependent systems using time Petrinets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, X., Hu, J., Bu, L., Zhao, J., Zheng, G. (2005). Consistency Checking of Concurrent Models for Scenario-Based Specifications. In: Prinz, A., Reed, R., Reed, J. (eds) SDL 2005: Model Driven. SDL 2005. Lecture Notes in Computer Science, vol 3530. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11506843_21
Download citation
DOI: https://doi.org/10.1007/11506843_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26612-9
Online ISBN: 978-3-540-31539-1
eBook Packages: Computer ScienceComputer Science (R0)