Transforming sources to petri nets: a way to analyze execution of parallel programs

ABSTRACT

Model checking is a suitable formal technique to analyze parallel programs' execution in an industrial context because automated tools can be designed and operated with very limited knowledge of the underlying techniques. However, the specification must be given using dedicated notations that are not always familiar to engineers (so far, model checking on UML raises complex problems that will not be solved immediately).

This paper proposes an approach to perform transformation of source code (C programs) into Petri nets, a suitable specification for model checking. To overcome the complexity of the resulting specification, we focus on specific aspects of the program. So, several transformations can be performed to verify some aspects of the processed programs. Parts of this approach could be reused by intrusion detection systems.

REFERENCES

• 1: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, v.36 n.5, p.203-213, May 2001
• 2: B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, and P. McKenzie. Systems and Software Verification: Model-Checking Techniques and Tools, chapter Model Cjhecking, pages 39--46. Springer Verlag, 2001.
• 3: David Binkley, Source Code Analysis: A Road Map, 2007 Future of Software Engineering, p.104-119, May 23-25, 2007 [doi>10.1109/FOSE.2007.27]
• 4: L. Brim. Parallel model-checking. ERCIM news, special section on Automated Software Engineering, 58:35, July 2004.
• 5: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 6: E. Clarke, O. Grumberg, and A. Peled. Model Checking. MIT Press, 2000.
• 7: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 8: Brian Cole , Daniel Hakim , David Hovemeyer , Reuven Lazarus , William Pugh , Kristin Stephens, Improving your software using static analysis to find bugs, Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA [doi>10.1145/1176617.1176667]
• 9: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 10: H. Debar. An introduction to intrusion-detection systems. In Proceedings of Connect '2000, Doha, Qatar, April 29th-May 1st, 2000, 2000.
• 11: E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta Inf., 1:115--138, 1971.
• 12: Matthew B. Dwyer , John Hatcliff , Robby Robby , Corina S. Pasareanu , Willem Visser, Formal Software Analysis Emerging Trends in Software Model Checking, 2007 Future of Software Engineering, p.120-136, May 23-25, 2007 [doi>10.1109/FOSE.2007.6]
• 13: S. Edelkamp, S. Leue, A. Lluch-Lafuente, and W. Visser. Dagstuhl Seminar on Directed Model Checking, April 2006.
• 14: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: C. Girault and R. Valk. Petri Nets for Systems Engineering. Springer Verlag - ISBN: 3-540-41217-4, 2003.
• 16: Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005 [doi>10.1007/s10703-005-1489-x]
• 17: Luqi , Joseph A. Goguen, Formal Methods: Promises and Problems, IEEE Software, v.14 n.1, p.73-85, January 1997 [doi>10.1109/52.566430]
• 18: Serge Haddad, A reduction theory for coloured nets, Advances in Petri Nets 1989, covers the 9th European Workshop on Applications and Theory in Petri Nets-selected papers, p.209-235, June 01, 1988
• 19: K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. STTT, 2(4):366--381, 2000.
• 20: L. Hillah, F. Kordon, L. Petrucci, and N. Trèves. PN standardisation: a survey. In International Conference on Formal Methods for Networked and Distributed Systems (FORTE '06), pages 307--322, Paris, France, September 2006. IFIP.
• 21: G. Holzmann. The SPIN model checker, chapter An Overview of PROMELA, pages 33--72. Addison-Wesley, 2004.
• 22: Gerard J. Holzmann , Margaret H. Smith, A practical method for verifying event-driven software, Proceedings of the 21st international conference on Software engineering, p.597-607, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302710]
• 23: Fabrice Kordon , Jean-Baptiste Voron, Rapid Prototyping of Intrusion Detection Systems, Proceedings of the 18th IEEE/IFIP International Workshop on Rapid System Prototyping, p.89-98, May 28-30, 2007 [doi>10.1109/RSP.2007.34]
• 24: Henryk Krawczyk , B. Wiszniewski, Analysis and Testing of Distributed Software Applications, Taylor & Francis, Inc., Bristol, PA, 1998
• 25: Move-Team. The CPN-AMI Home page, http://www.lip6.fr/cpn-ami, 2006.
• 26: Frank Tip, A Survey of Program Slicing Techniques., CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1994
• 27: K. Varpaaniemi. Prod: An advanced tool for efficient reachability analysis. http://www.tcs.hut.fi/Software/prod.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Model checking

General Terms:
Design, Reliability, Verification

Keywords:
GCC, petri nets, software analysis