Modelling in the contexts of verification and design/10. Problem Frames.

Problem frames provide a good possibility for systematic decomposition. They can be presented in a graphical form that supports intuition. It is easy to combine problem frames with any other formalism, such as automata, to describe behavioural (or other) aspects of components in detail.

(of course, much more can be said over problem frames...)