SIG-SoS

Slicing Promela and its applications to model checking, simulation, and protocol understanding

작성자
selab
작성일
2016-09-06 04:17
조회
191
Title: Slicing Promela and its applications to model checking, simulation, and protocol understanding

Published In: Proceedings of the 4th International SPIN Workshop. 1998.

Authors: Millett, Lynette I., Tim Teitelbaum

Abstract:
Static program slicing has been used effectively for a variety of applications ranging from debugging to program integration to software re-engineering. A program slice consists of the parts of a program that may affect or are affected by the value being computed at the point of interest. A slice, for sequential programs, is computed by examining control and data dependence in the program. Recent work in slicing concurrent programs examines how values at a particular program point are affected by synchronization, communication, and non-determinism (along with the traditional control and data dependence effects.) We are extending this work to slice the Promela programming language, used to specify protocols for the Spin model checker. Another application of slicing may be its usefulness in paring down protocol descriptions to just the pieces that affect particular points of interest (e.g. assertion statements, never claims, etc. in Promela). Model checking and simulation of the pared-down protocol may, in some cases, be much more efficient. We present program slicing as a tool that, along with model checking and simulation techniques, can facilitate understanding and debugging of protocols.