SOC: a slicer for CSP specifications

ABSTRACT

This paper describes SOC, a program slicer for CSP specifications. In order to increase the precision of program slicing, SOC uses a new data structure called Context-sensitive Synchronized Control Flow Graph (CSCFG). Given a CSP specification, SOC generates its associated CSCFG and produces from it two different kinds of slices; which correspond to two different static analyses. We present the tool's architecture, its main applications and the results obtained from experiments conducted in order to measure the performance of the tool.

REFERENCES

• 1: D. Binkley and K. B. Gallagher. Program slicing. Advances in Computers, 43:1--50, 1996.
• 2: M. Butler and M. Leuschel. Combining CSP and B for specification and property verification. In Proceedings of Formal Methods 2005, LNCS 3582, pages 221--236, Newcastle upon Tyne, 2005. Springer-Verlag.
• 3: David Callahan , Jaspal Sublok, Static analysis of low-level synchronization, Proceedings of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and distributed debugging, p.100-111, May 05-06, 1988, Madison, Wisconsin, United States
• 4: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.26 n.1, p.100-106, Jan. 1983 [doi>10.1145/357980.358021]
• 5: Michael Leuschel , Michael Butler, ProB: an automated analysis toolset for the B method, International Journal on Software Tools for Technology Transfer (STTT), v.10 n.2, p.185-203, February 2008 [doi>10.1007/s10009-007-0063-9]
• 6: Michael Leuschel , Marc Fontaine, Probing the Depths of CSP-M: A New fdr-Compliant Validation Tool, Proceedings of the 10th International Conference on Formal Methods and Software Engineering, October 27-31, 2008, Kitakyushu-City, Japan [doi>10.1007/978-3-540-88194-0_18]
• 7: M. Leuschel, M. Llorens, J. Oliver, J. Silva, and S. Tamarit. Static slicing of CSP specifications. In Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'08), pages 141--150, 2008.
• 8: M. Leuschel, M. Llorens, J. Oliver, J. Silva, and S. Tamarit. The MEB and CEB static analysis for CSP specifications. Technical report, Department of Computer Science, Technical University of Valencia. Accessible via http://www.dsic.upv.es/~jsilva, Valencia, Spain, October 2008.
• 9: F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.
• 10: Mark David Weiser, Program slices: formal, psychological, and practical investigations of an automatic program abstraction method, University of Michigan, Ann Arbor, MI, 1979

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages, Theory

Keywords:
program slicing, software engineering