[en] High-level Petri nets (evolutions of low-level Petri nets) are well suitable formalisms to represent complex data, which influence the behavior of distributed, concurrent systems. However, usual verification techniques such as model checking and testing remain an open challenge for both (i.e., low-level and high-level Petri nets) because of the state space explosion problem and test case selection. The contribution of this paper is to propose a technique to improve the model checking and test- ing of systems modeled using Algebraic Petri nets (a variant of high-level petri nets). To achieve the objective, we propose different slicing algo- rithms for Algebraic Petri nets. We argue that our slicing algorithms significantly improve the state of the art related to slicing APNs and can also be applied to low-level Petri nets with slight modifications. We exemplify our proposed algorithms through a case study of a car crash management system.
Disciplines :
Computer science
Author, co-author :
Khan, Yasir Imtiaz ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Guelfi, Nicolas ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Language :
English
Title :
Slicing High-level Petri nets
Publication date :
23 June 2014
Event name :
International Workshop on Petri Nets and Software Engineering (PNSE'14)
Event place :
TUNIS, Tunisia
Event date :
23-06-2014 TO 27-06-2014
Audience :
International
Main work title :
International Workshop on Petri Nets and Software Engineering (PNSE'14), Tunis June 2014
D. Buchs, S. Hostettler, A. Marechal, and M. Risoldi. Alpina: A symbolic model checker. In J. Lilius and W. Penczek, editors, Applications and Theory of Petri Nets, volume 6128 of Lecture Notes in Computer Science, pages 287-296. Springer Berlin Heidelberg, 2010.
J. R. Burch, E. Clarke, K. L. McMillan, D. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e, pages 428-439, 1990.
J. Chang and D. J. Richardson. Static and dynamic specification slicing. In In Proceedings of the Fourth Irvine Software Symposium, 1994.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8:244-263, 1986.
K. Jensen. Coloured petri nets. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Petri Nets: Central Models and Their Properties, volume 254 of Lecture Notes in Computer Science, pages 248-299. Springer Berlin Heidelberg, 1987.
Y. I. Khan. A formal approach for engineering resilient car crash management system. Technical Report TR-LASSY-12-05, University of Luxembourg, 2012.
Y. I. Khan. Optimizing verification of structurally evolving algebraic petri nets. In V. K. A. Gorbenko, A. Romanovsky, editor, Software Engineering for Resilient Systems, volume 8166 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2013.
Y. I. Khan. Optmizing algebraic petri net model checking by slicing. Technical Report TR-LASSY-13-02, University of Luxembourg, 2013.
Y. I. Khan. Slicing high-level petri nets. Technical Report TR-LASSY-14-03, University of Luxembourg, 2014.
Y. I. Khan and M. Risoldi. Optimizing algebraic petri net model checking by slicing. International Workshop on Modeling and Business Environments (ModBE'13, associated with Petri Nets'13), 2013.
L. Lamport. What good is temporal logic. Information processing, 83:657-668, 1983.
W. J. Lee, H. N. Kim, S. D. Cha, and Y. R. Kwon. A slicing-based approach to enhance petri net reachability analysis. Journal of Research Practices and Information Technology, 32:131-143, 2000.
M. Llorens, J. Oliver, J. Silva, S. Tamarit, and G. Vidal. Dynamic slicing techniques for petri nets. Electron. Notes Theor. Comput. Sci., 223:153-165, Dec. 2008.
A. Rakow. Slicing petri nets with an application to workflow verification. In Proceedings of the 34th conference on Current trends in theory and practice of computer science, SOFSEM'08, pages 436-447, Berlin, Heidelberg, 2008. Springer- Verlag.
A. Rakow. Slicing and Reduction Techniques for Model Checking Petri Nets. PhD thesis, University of Oldenburg, 2011.
A. Rakow. Safety slicing petri nets. In S. Haddad and L. Pomello, editors, Application and Theory of Petri Nets, volume 7347 of Lecture Notes in Computer Science, pages 268-287. Springer Berlin Heidelberg, 2012.
W. Reisig. Petri nets and algebraic specifications. Theor. Comput. Sci., 80(1):1-34, 1991.
K. Schmidt. T-invariants of algebraic petri nets. Informatik- Bericht, 1994.
F. Tip. A survey of program slicing techniques. JOURNAL OF PROGRAMMING LANGUAGES, 3:121-189, 1995.
A. Valmari. The state explosion problem. In Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, pages 429-528, London, UK, UK, 1998. Springer-Verlag.
Y. Wangyang, Y. Chungang, D. Zhijun, and F. Xianwen. Extended and improved slicing technologies for petri nets. High Technology Letters, 19(1), 2013.
M. Weiser. Program slicing. In Proceedings of the 5th international conference on Software engineering, ICSE '81, pages 439-449, Piscataway, NJ, USA, 1981. IEEE Press.
B. Xu, J. Qian, X. Zhang, Z. Wu, and L. Chen. A brief survey of program slicing. SIGSOFT Softw. Eng. Notes, 30(2):1-36, Mar. 2005.
