Based on SAM, we have developed constraint-driven incremental verification methods that have the following characteristics:

1. It provides concrete procedure(s) to guide the verification process.
2. It supports composition of analysis results on individual system components to obtain system-wide property at a given design level (Horizontal composition-ability).
3. Third, it supports incremental verification across different design levels by systematically decomposing and propagating high-level system constraints to lower-level designs in such a way that a verified lower-level design can be safely plugged into its parent level architecture without having to re-verify the entire model (Vertical composition-ability).

In particular, our investigation is proceeding along two directions:

1. We are continuing to expand our constraint-driven component-level Petri nets reduction techniques, which are significantly more efficient than conventional Petri net reduction techniques. Main objective here is twofold:

• to achieve same degree of reduction with less restrictions so that they can be applied to more general design models.
• to develop component-level reduction rules that are applicable to other system properties, e.g. performance.

2. We are investigating analysis methods that effectively utilize and leverage existing techniques of model checking, which are more systematic and scalable. To achieve this objective, we need to develop algorithms to verify consistency between system constraints at different levels of abstraction.

• exploit the compositional nature of SAM framework to develop model checking algorithms that lets us analyze components one at a time and then compose these results to deduce global properties about the entire system.
• use environmental constraints to reduce the state space of a system thereby increasing the efficiency of the verification algorithm.
• use environmental constraints to reduce the state space of a system thereby increasing the efficiency of the verification algorithm.