• 1. Roscoe, A.W.: Understanding concurrent systems. Springer (2010).
    @book{Roscoe2010,
      title = {{U}nderstanding concurrent systems},
      author = {Roscoe, Andrew William},
      publisher = {Springer},
      year = {2010},
      owner = {pfr500},
      timestamp = {2013.12.10}
    }
    
  • 2. Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for \sf\slshape Circus\normalfont. Formal Aspects of Computing. 15, 146–181 (2003).

    We present a refinement strategy for Circus, which is the combination of Z, CSP, and the refinement calculus in the setting of Hoare and He’s unifying theories of programming. The strategy unifies the theories of refinement for processes and their constituent actions, and provides a coherent technique for the stepwise refinement of concurrent and distributed programs involving rich data structures. This kind of development is carried out using Circus’s refinement calculus, and we describe some of its laws for the simultaneous refinement of state and control behaviour, including the splitting of a process into parallel subcomponents. We illustrate the strategy and the laws using a case study that shows the complete development of a small distributed program.

    @article{Cavalcanti2003,
      title = {{A} {R}efinement {S}trategy for \sf\slshape {C}ircus\normalfont},
      author = {Cavalcanti, Ana and Sampaio, Augusto and Woodcock, Jim},
      journal = {Formal Aspects of Computing},
      year = {2003},
      pages = {146-181},
      volume = {15},
      affiliation = {Computing Laboratory University of Kent at Canterbury Canterbury CT2 7NF UK},
      doi = {10.1007/s00165-003-0006-5},
      issn = {0934-5043},
      issue = {2},
      keyword = {Computer Science},
      owner = {Cathode},
      publisher = {Springer London},
      timestamp = {2011.01.30},
      url = {http://dx.doi.org/10.1007/s00165-003-0006-5}
    }
    
  • 3. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998).
    @book{Hoare1998,
      title = {{U}nifying {T}heories of {P}rogramming},
      author = {Hoare, C. A. R. and He, Jifeng},
      publisher = {Prentice Hall International Series in Computer Science},
      year = {1998},
      owner = {Cathode},
      timestamp = {2011.01.30}
    }
    
  • 4. Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall (1996).
    @book{Woodcock1996,
      title = {{U}sing {Z}: {S}pecification, {R}efinement, and {P}roof},
      author = {Woodcock, Jim and Davies, Jim},
      publisher = {Prentice Hall},
      year = {1996},
      owner = {Cathode},
      timestamp = {2011.01.30}
    }