In: Proc. 31-st Annual Hawaii Int. Conf. on System Sciences; Vol. 7: Software Technology Track, 6-9 January 1998, Kohala Coast, HI, pages 404-414. 1998. Available at http://www.informatik.uni-hildesheim.de/~pep.
Abstract: In this paper, a new method for proving qualitative properties of SDL-systems is presented, which is based on a compositional high-level Petri net semantics for SDL. Since emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures, our method is especially interesting for typical client-server systems.
By using M-nets as the semantic model we are able to use `state of the art' verification techniques. For instance, the verification component of the PEP tool may be applied which presently includes partial order based model checking and algorithms based on linear programming as well as interfaces to other verification packages such as INA, SMV and SPIN providing reduction algorithms based on BDDs, on the stubborn set or sleep set method, and on symmetries.
We show the benefits of our method applying it to a typical client-server system. After describing how safety, liveness and progress properties can be checked fully automatically, we give examples how the compositional nature of the M-net semantics can be used to solve the `state explosion' problem, and how interactive verification may extend the verification possibilities.
Keywords: Compositionality; Concurrency; Dynamic Processes; Petri Net Semantics; Procedures; SDL; Verification.
Back to the Petri Nets Bibliography