We propose and study a framework for systematic
development of software systems (or models) from their
We introduce a language for refinement and branching of formal
developments. We complement it with a notion of refinement tree and present
proof calculi for checking correctness of refinements as well as
their consistency. Both calculi have been implemented in the
Heterogeneous Tool Set (Hets), and have been integrated with other
tools like model finders and conservativity checkers.