Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Relaxing Property Preservation in the Refinement of Concurrent Systems

    2nd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th July 1997


    M. Siegel


    One of the major development strategies for concurrent systems suggests to start the system development from a so called functional design of the envisaged system and to distribute/parallelize this design in subsequent development steps towards a concurrent system.

    In this paper we argue that this strategy is not supported by the standard state-based refinement approaches.

    This phenomenon is traced back to the fact that these approaches are constructed such that necessarily all temporal properties of the refined system are preserved during refinement.

    We explain that the key feature of a suitable refinement notion for the above strategy has to relax this strict preservation of properties.

    Rather than preserving all temporal properties of the refined system the required refinement notion has to support the exclusive preservation of specific properties.

    We present such a refinement approach and prove that the standard state-based refinement relations are particular instances of the advocated notion.


    PDF filePDF Version of this Paper (185kb)