Abstract
Grading dozens of Petri net models manually is a tedious and error-prone task. In this paper, we present Grade/CPN, a tool supporting the grading of Colored Petri nets modeled in CPN Tools. The tool is extensible, configurable, and can check static and dynamic properties. It automatically handles tedious tasks like checking that good modeling practise is adhered to, and supports tasks that are difficult to automate, such as checking model legibility. We propose and support the Britney Temporal Logic which can be used to guide the simulator and to check temporal properties. We provide our experiences with using the tool in a course with 100 participants.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Jensen, K., Kristensen, L.M.: Coloured Petri Nets – Modelling and Validation of Concurrent Systems. Springer (2009)
van der Aalst, W.M.P., Stahl, C.: Modeling Business Processes – A Petri Net-Oriented Approach. MIT Press (2011)
Online: CPN Tools webpage, http://cpntools.org
Westergaard, M., Kristensen, L.M.: The Access/CPN Framework: A Tool for Interacting with the CPN Tools Simulator. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 313–322. Springer, Heidelberg (2009)
Westergaard, M., Fahland, D., Stahl, C.: Grade/CPN: Semi-automatic Support for Teaching Petri Nets by Checking Many Petri Nets Against One Specification. In: Proc. of PNSE. CEUR Workshop Proceedings, vol. 851, pp. 32–46. CEUR-WS.org (2012)
Westergaard, M., Evangelista, S., Kristensen, L.M.: ASAP: An Extensible Platform for State Space Analysis. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 303–312. Springer, Heidelberg (2009)
Pnueli, A.: The Temporal Logic of Programs. In: Proc. of SFCS 1977, pp. 46–57. IEEE Comp. Soc. (1977)
Kripke, S.A.: A semantical analysis of modal logic: I. Normal modal propositional calculi. Zeitschrift fŭr Mathematische Logic und Grundlagen der Mathematik 9, 67–96 (1963)
Plotkin, G.: A Structural Approach to Operational Semantics. DAIMI-FN 19, Department of Computer Science, University of Aarhus (1981)
Giannakopoulou, D., Havelund, K.: Automata-Based Verification of Temporal Properties on Running Programs. In: Proc. ASE, pp. 412–416. IEEE Computer Society (2001)
Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers (2006)
Weißleder, S.: Simulated satisfaction of coverage criteria on uml state machines. In: ICST 2012, pp. 117–126 (2010)
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL Semantics for Runtime Verification. Logic and Computation 20(3), 651–674 (2010)
Online: JUnit webpage, http://junit.org
Online: Jenkins Continuous Integration webpage, http://jenkins-ci.org
Ihantola, P., Ahoniemi, T., Karavirta, V., Seppälä, O.: Review of Recent Systems for Automatic Assessment of Programming Assignments. In: Proc. International Conference on Computing Education Research, pp. 86–93. ACM (2010)
Verhoeff, T.: Programming Task Packages: Peach Exchange Format. Olympiads in Informnatics 2, 192–207 (2008)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Form. Methods Syst. Des. 19(1), 45–80 (2001)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM 50, 752–794 (2003)
Edelkamp, S., Lluch Lafuente, A., Leue, S.: Directed Explicit Model Checking with HFS-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
ISO/IEC: Software and system engineering – High-level Petri nets – Part 2: Transfer format. ISO/IEC 15909-2:2011
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Westergaard, M., Fahland, D., Stahl, C. (2013). Grade/CPN: A Tool and Temporal Logic for Testing Colored Petri Net Models in Teaching. In: Koutny, M., van der Aalst, W.M.P., Yakovlev, A. (eds) Transactions on Petri Nets and Other Models of Concurrency VIII. Lecture Notes in Computer Science, vol 8100. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40465-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-40465-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40464-1
Online ISBN: 978-3-642-40465-8
eBook Packages: Computer ScienceComputer Science (R0)