An approach for specification construction using property-preserving refinement patterns

ABSTRACT

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.

REFERENCES

• 1: R. J. R. Back, A calculus of refinements for program derivations, Acta Informatica, v.25 n.6, p.593-624, Aug. 1988 [doi>10.1007/BF00291051]
• 2: R. Back and K. Sere. Superposition refinement of reactive systems. Formal Aspects of Computing, pages 324--346, August 1996.
• 3: Wilfried Brauer , Robert Gold , Walter Vogler, A survey of behaviour and equivalence preserving refinements of Petri nets, Proceedings on Advances in Petri nets 1990, p.1-46, March 1991
• 4: David Garlan, Style-based refinement for software architecture, Joint proceedings of the second international software architecture workshop (ISAW-2) and international workshop on multiple perspectives in software development (Viewpoints '96) on SIGSOFT '96 workshops, p.72-75, October 16-18, 1996, San Francisco, California, United States [doi>10.1145/243327.243607]
• 5: H. J. Genrich, Equivalence transformations of PrT-nets, Advances in Petri nets 1989, Springer-Verlag New York, Inc., New York, NY, 1990
• 6: Xudong He, Transformations on Hierarchical Predicate Transition Nets: Refinements and Abstractions, Proceedings of the 22nd International Computer Software and Applications Conference, p.164-171, August 19-21, 1998
• 7: X. He and Y. Deng. Specifying software archtectural connectors in SAM. International Journal of Software Engineering and Knowledge Engineering, 10(4):411--431, 2000.
• 8: X. He and Y. Deng. A framework for developing and analyzing software architecture sepcifications in SAM. The Computer Journal, 45(1):111--128, 2002.
• 9: Mark Moriconi , Xiaolei Qian , R. A. Riemenschneider, Correct Architecture Refinement, IEEE Transactions on Software Engineering, v.21 n.4, p.356-3, April 1995 [doi>10.1109/32.385972]
• 10: Julia Padberg , Kathrin Hoffmann , Magdalena Gajewsky, Stepwise Introduction and Preservation of Safety Properties in Algebraic High-Level Net Systems, Proceedings of the Third Internationsl Conference on Fundamental Approaches to Software Engineering: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.249-265, March 25-April 02, 2000
• 11: J. Padberg and M. Urbasek. Rule-based refinement of petri nets: A survey. In H. Ehrig, W. Reisig, G. Rozenberg, and H. Weber, editors, Advances in Petri Nets: Petri Net Technologies for Modeling Communication Based Systems, Springer LNCS. Springer, 2002.
• 12: M. Urbasek and J. Padberg. Preserving liveness with rule-based refinement of place/transition systems. In Proc. of Sixth World Conference on Integrated Design and Process Technology (IDPT'02), Pasadensa, USA, 2002.
• 13: J. Wang, X. He, and Y. Deng. Introducing software architecture specification and analysis in SAM through an example. Information and Software Technology, 41:451--467, 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.7 Distribution, Maintenance, and Enhancement
          Subjects: Restructuring, reverse engineering, and reengineering

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
        D.2.11 Software Architectures
      D.2.4 Software/Program Verification
          Subjects: Validation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Design, Management, Verification

Keywords:
property-preserving, refinement, software architecture