An approach for specification construction using property-preserving refinement patterns
Junhua Ding, Lian Mo, Xudong He · 2008
This paper proposes a refinement method based on a set of formal refinement patterns for software architecture design using Software Architecture Model (SAM). First, an approach for specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. Then, modeling and refining a life insurance system is used to demonstrate how to applying the refinement patterns for software architecture design using SAM. The results demonstrate that a refinement method is an effective way to develop a high assurance system. Our result can be easily generalized to other formal methods as well.