Stratified operational semantics for safety and correctness of the region calculus