This paper deals with the problem of the usage of formal
techniques, based on model checking, where models are large and formal
verification techniques face the combinatorial explosion issue. The goal
of the approach is to express and verify requirements relative to certain
context situations. The idea is to unroll the context into several scenarios
and successively compose each scenario with the system and verify
the resulting composition. We propose to specify the context in which
the behavior occurs using a language called CDL (Context Description
Language), based on activity and message sequence diagrams. The properties
to be verified are specified with textual patterns and attached to
specific regions in the context. The central idea is to automatically split
each identified context into a set of smaller subcontexts and to compose
them with the model to be validated. For that, we have implemented a recursive
splitting algorithm in our toolset OBP (Observer-based Prover).
This paper shows how this combinatorial explosion could be reduced by
specifying the environment of the system to be validated.
An Spin / Promela Application for Model checking UML Sequence Diagrams
