Abstract
This paper proposes an on-the-fly linear temporal logic model checker using state-space generation based on Petri net models. The hierarchical Petri net simulator (HiPS) tool, developed by our research group at Shinshu University, is a design and verification environment for Place/Transition nets and is capable of generating state-space and trace-process graphs. In combination with external tools, HiPS can perform exhaustive model checking for a state space. However, exhaustive model checking is required for generating a complete state space. On-the-fly model checking is an approach for solving the explosion problem to generate a portion of the overall state space by parallelizing the search and generation processes. In this study, we propose a model checker for a Petri net model to concurrently function with state-space generation using an interprocess communication channel. By utilizing the concept of fluency, we implement automata-based model checking for Petri nets. This implementation achieves high-efficiency for on-the-fly verification, which is independent of the verification and state-space generation processes.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
ISO. (1989). Information processing systems – Open systems interconnection – LOTOS: A formal description technique based on the temporal ordering of observational behaviour. Geneve: International Organization for Standardization. Technical Report 8807:1989.
Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21(8), 666–677. [Online]. Available: http://doi.acm.org/10.1145/359576.359585.
Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77, 541–580.
Reisig, W. (1985). Petri nets: An introduction (EATCS monographs on theoretical computer science, Vol. 4). Berlin/New York: Springer.
Westergaard, M., & Verbeek, H. E. CPN tools. http://cpntools.org/.
Dingle, N., & Knottenbelt, W. Platform independent petri net editor 2. http://pipe2.sourceforge.net/.
University, S. (2016) Hips – Hierarchical petri net simulator. [Online]. Available: http://sourceforge.net/projects/hips-tools/.
VASY/INRIA. (2015) CADP toolbox. [Online]. Available: http://cadp.inria.fr/.
Clarke, E. M., Grumberg, O., & Peled, D. (2001). Model checking. Cambridge: MIT Press.
Ohta, I., & Wasaki, K. (2013). Model designing using a Petri net tool and state space generation algorithm for post-verification tool. In 12th Forum on Information Technology, FIT2013 (pp. 171–174).
Schwoon, S., & Esparza, J. (2005). A note on on-the-fly verification algorithms. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS2005 (pp. 174–190).
Giannakopoulou, D., & Magee, J. (2003). Fluent model checking for event-based systems. In Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering, 2003. (pp. 257–266). ACM.
Harie, Y., & Wasaki, K. (2015). On-the-fly LTL model checker on the Petri net design tool: HiPS. In 14th Forum on Information Technology, FIT2015 (pp. 139–142).
Gastin, P., & Oddoux, D. (2001). Fast LTL to büchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification, CAV2001 (pp. 53–65).
Stevens, W. R., Fenner, B., & Rudoff, A. M. (2003). UNIX network programming (Vol. 1, 3rd ed.). Delhi: Pearson Education.
Tel, G. (2001). Introduction to distributed algorithms (2nd ed.). New York: Cambridge University Press.
laboratory, S. (2015). Spec patterns. [Online]. Available: http://patterns.projects.cis.ksu.edu/.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Harie, Y., Wasaki, K. (2018). A Petri Net Design and Verification Platform Based on The Scalable and Parallel Architecture: HiPS. In: Latifi, S. (eds) Information Technology - New Generations. Advances in Intelligent Systems and Computing, vol 558. Springer, Cham. https://doi.org/10.1007/978-3-319-54978-1_37
Download citation
DOI: https://doi.org/10.1007/978-3-319-54978-1_37
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-54977-4
Online ISBN: 978-3-319-54978-1
eBook Packages: EngineeringEngineering (R0)