| It is commonly accepted that a major impediment to static analysis of concurrent programs is the complexity associated with producing various forms of state space representations. The goal of the current work is to develop analysis techniques which give reasonable performance for systems of practical size by systematically optimizing the underlying models, Petri nets derived from Ada-tasking programs. This optimization is based on two key ingredients: Focusing on a specific analysis issue such as deadlock, and adapting an existing model-reduction technique, Petri net reduction. By combining Petri net theory and knowledge of Ada-tasking semantics, we derive some domain-specific reduction rules for Petri net models of Ada-tasking. These rules allow us to reduce the size of a program model while preserving the model's properties such as deadlock characteristics. When a potential deadlock state is detected, an interpretation that helps the user to understand this detected scenario is necessary. In order to provide for a reduced net sufficient information to support this kind of interpretation, a method is suggested based on the Petri net state equation. Since every reduction rule in our rule set is linear, the complexity to complete net reduction for a net model is polynomial. Experiments with our prototype tool for the reduction rules show good performance. |
