Refinement patterns for ASTDs

This paper introduces three refinement patterns for algebraic state-transition diagrams (astds): state refinement, transition refinement and loop-transition refinement. These refinement patterns are derived from practice in using astds for specifying information systems and security policies in two industrial research projects. Two refinement relations used in these patterns are formally defined. For each pattern, proof obligations are proposed to ensure preservation of behaviour through refinement. The proposed refinement relations essentially consist in preserving scenarios by replacing abstract events with concrete events, or by introducing new events. Deadlocks cannot be introduced; divergence over new events is allowed in one of the refinement relation. We prove congruence-like properties for these three patterns, in order to show that they can be applied to a subpart of a specification while preserving global properties. These three refinement patterns are illustrated with a simple case study of a complaint management system.