Prosega/CPN: An Extension of CPN Tools for Automata-based Analysis and System Verification
https://doi.org/10.15514/ISPRAS-2018-30(4)-7
Abstract
The verification and analysis of distributed systems is a task of utmost importance, especially in today’s world where many critical services are completely supported by different computer systems. Among the solutions for system modelling and verification, it is particularly useful to combine the usage of different analysis techniques. This also allows the application of the best formalism or technique to different components of a system. The combination of Colored Petri Nets (CPNs) and Automata Theory has proved to be a successful formal technique in the modelling and verification of different distributed systems. In this context, this paper presents Prosega/CPN ( Protocol Sequence Generator and Analyzer ), an extension of CPN Tools for supporting automata-based analysis and verification. The tool implements several operations such as the generation of a minimized deterministic finite-state automaton (FSA) from a CPN’s occurrence graph, language generation, and FSA comparison. The solution is supported by the Simulator Extensions feature whose development has been driven by the need of integrating CPN with other formal methods. Prosega/CPN is intended to support a formal verification methodology of communication protocols; however, it may be used in the verification of other systems whose analysis involves the comparison of models at different levels of abstraction. For example, business strategy and business processes. An insightful use case is provided where Prosega/CPN has been used to analyze part of the IEEE 802.16 MAC connection management service specification.
About the Authors
J. C. Carrasquel
La Sapienza University of Rome
Italy
Italy
A. Morales
Central University of Venezuela
Venezuela, Bolivarian Republic of
Venezuela, Bolivarian Republic of
M. E. Villapol
Auckland University of Technology
New Zealand
New Zealand
References
1. T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, vol. 77, no. 4, April 1989, pp. 541–580
2. K. Jensen and L. M. Kristensen. Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Berlin, Heidelberg: Springer-Verlag, 2009
3. CPN Tools – A tool for editing, simulating, and analyzing Coloured Petri Nets. Available at: http://www.cpntools.org/, accessed: 20.06.2018
4. M. Westergaard. CPN Tools 4: Multi-formalism and Extensibility. In Application and Theory of Petri Nets and Concurrency. Berlin, Heidelberg: Springer-Verlag, 2013, pp. 400–409
5. M. E. Villapol. Modelling and Analysis of the Resource Reservation Protocol Using Coloured Petri Nets. Ph.D. dissertation, University of South Australia, Australia, December 2003
6. S. Gordon, L. M. Kristensen, and J. Billington. Verification of a Revised WAP Wireless Transaction Protocol, In Application and Theory of Petri Nets and Concurrency. Berlin, Heidelberg: Springer-Verlag, 2002, pp. 182–202
7. B. Han. Formal Specification of the TCP Service and Verification of TCP Connection Management. Ph.D. dissertation, University of South Australia, Australia, April 2004
8. J. Billington, G. E. Gallasch, and B. Han. A Coloured Petri Net Approach to Protocol Verification. Berlin, Heidelberg: Springer-Verlag, 2004, pp. 210–290.
9. G. Gallasch and L. M. Kristensen. Comms/CPN: A Communication Infrastructure for External Communication with Design/CPN. In Proc. of the Third Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB-554, pages 75–91
10. M. Westergaard and K. B. Lassen. The BRITNeY Suite Animation Tool. In Applications and Theory of Petri Nets and Concurrency. Berlin, Heidelberg: Springer-Verlag, 2006, pp. 431–440
11. M. Westergaard. Access/CPN 2.0: A High-Level Interface to Coloured Petri Net Models. In Application and Theory of Petri Nets and Con- currency. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 328–337
12. AT&T Researchers – Inventing the Science Behind the Service. Available at: http: //www.research.att.com/evergreen/portfolio/, accessed: 20.06.2018
13. OpenFST Library. Available at: http://www.openfst.org/twiki/bin/view/FST/WebHome, accessed: 20.06.2018
14. M. Hulden. Foma: A Finite-state Compiler and Library. In Proceedings of the 12th Conference of the European Chapter of the Association for Computational Linguistics: Demonstrations Session. Stroudsburg, PA, USA: Association for Computational Linguistics, 2009, pp. 29–32
15. A. Almeida, M. Almeida, J. Alves, N. Moreira, and R. Reis. FAdo and GUItar: Tools for Automata Manipulation and Visualization. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2009, pp. 65–74
16. S. H. Rodger. JFLAP: An Interactive Formal Languages and Automata Package. USA: Jones and Bartlett Publishers, Inc., 2006
17. C. Ouyang and J. Billington. Formal Analysis of the Internet Open Trading Protocol. In Applying Formal Methods: Testing, Performance, and M/E-Commerce. Berlin, Heidelberg: Springer-Verlag, 2004, pp. 1–15
18. S. Barzegar, M. Davoudpour, M. R. Meybodi, A. Sadeghian, and M. Tirandazian. Traffic Signal Control with Adaptive Fuzzy Coloured Petri Net Based on Learning Automata. In Annual Meeting of the North American Fuzzy Information Processing Society, July 2010, pp. 1–8
19. N. Danapaquiame, E. Ilavarasan, N. Kumar, and S. K. Dwivedi. Ratification strategy for web service composition using CPN: A survey. In Proc. of the IEEE International Conference on Computational Intelligence and Computing Research, December 2013, pp. 1–4
20. J. Zhu, K. Zhang, and G. Zhang. Verifying Web Services Composition based on LTL and colored Petri Net. In Proc. of the 6th International Conference on Computer Science Education, August 2011, pp. 1127–1130
21. ISO/IEC. High-level Petri Nets – Part 1: Concepts, Definitions and Graphical Notation. Software and Systems Engineering, ISO/IEC FDIS 15909-1. Final Draft International.
22. W. A. Barrett and J. D. Couch. Compiler Construction: Theory and Practice. Chicago, Illinois: Science Research Associates Inc., 1979
23. M. Westergaard. CPN Tools 4 Extensions: Part 4: Advanced Communication and Debugging. Available at: https://westergaard.eu/2013/11/cpn-tools-4-extensions-part-4-advanced-communication-and-debugging/, November 2013, Blog entry/, accessed: 20.06.2018
24. C. Allauzen, M. Riley, J. Schalkwyk, W. Skut, and M. Mohri. OpenFst: A General and Efficient Weighted Finite-State Transducer Library. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2007, pp. 11–23.
25. Graphviz – Graph Visualization Software. Available at: http://www.graphviz.org//, accessed: 20.06.2018
26. J. C. Carrasquel. Java/PROSEGA: An extension in CPN Tools for generating languages accepted by FSA and minimized deterministic FSA from a state space. Central University of Venezuela, Caracas, Venezuela, Tech. Rep., October 2015.
27. IEEE 802.16 Working Group on Broadband Wireless Access Standards. IEEE Std. 802.16e-2005. Local and Metropolitan Area Network. Part 16: Air Interface for Fixed and Mobile Broadband Wireless Access Systems
28. A. V. Morales and M. E. Villapol. Towards Formal Specification of the Service in the IEEE 802.16 MAC Layer for Connection Management. In Proceedings of the 9th WSEAS International Conference on Computational Intelligence, Man-machine Systems and Cybernetics. World Scientific and Engineering Academy and Society (WSEAS), 2010, pp. 140–146
29. A. V. Morales and M. E. Villapol. Reviewing the Service Specification of the IEEE 802.16 MAC Layer Connection Management: A Formal Approach. CLEI Electronic Journal, vol. 16, August 2013, pp. 1– 12
Review
For citations:
Carrasquel J.C., Morales A., Villapol M.E. Prosega/CPN: An Extension of CPN Tools for Automata-based Analysis and System Verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):107-128. https://doi.org/10.15514/ISPRAS-2018-30(4)-7
Email this article 