A Refinement Calculus for Circus - Mini-thesis

Book English OPEN
Oliveira, Marcel V. M.;
(2004)
  • Publisher: University of Kent
  • Subject: QA76
    acm: GeneralLiterature_MISCELLANEOUS

Most software developments do not use any of the existing theories and formalisms. This leads to a loss of precision and correctness on the resulting softwares. Two different approaches to formal techniques have been raised in the past decades: one focus on data aspects... View more
  • References (8)

    2 Circus 5 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.1 Circus Programs . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.2 Channel Declarations . . . . . . . . . . . . . . . . . . . . . . 6 2.1.3 Channel Set Declarations . . . . . . . . . . . . . . . . . . . . 7 2.1.4 Process Declarations . . . . . . . . . . . . . . . . . . . . . . 8 2.1.5 Compound Processes . . . . . . . . . . . . . . . . . . . . . . 9 2.1.6 Actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.1 The Unifying Theories of Programming . . . . . . . . . . . . 14 2.2.2 Circus Semantic Model . . . . . . . . . . . . . . . . . . . . . 16

    3 Refinement: Notions and Laws 23 3.1 Refinement Notions and Strategy . . . . . . . . . . . . . . . . . . . 24 3.2 Laws of Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.3 Process Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.4 Action Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.4.1 Laws on Prefixing . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4.2 Laws on Schemas . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4.3 Laws on Variable Blocks . . . . . . . . . . . . . . . . . . . . 32 3.4.4 Laws on Guards and Assumptions . . . . . . . . . . . . . . . 32 3.4.5 Laws on Parallelism . . . . . . . . . . . . . . . . . . . . . . . 32 3.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2.1 A Fibonacci Generator . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.1 An iteration of the refinement strategy . . . . . . . . . . . . . . . . 27

    [25] P.H.Welch, G.S.Stiles, G.H.Hilderink, and A.P.Bakkers. CSP for Java : Multithreading for All. In B.M.Cook, editor, Architectures, Languages and Techniques for Concurrent Systems, volume 57 of Concurrent Systems Engineering Series, Amsterdam, the Netherlands, April 1999. WoTUG, IOS Press.

    [26] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, 1998.

    [27] A. W. Roscoe, J. C. P. Woodcock, and L. Wulf. Non-interference through Determinism. In D. Gollmann, editor, ESORICS 94, volume 1214 of Lecture Notes in Computer Science, pages 33 - 54. Springer-Verlag, 1994.

    [28] ACA Sampaio, JCP Woodcock, and ALC Cavalcanti. Refinement in Circus. In L Eriksson and PA Lindsay, editors, FME 2002: Formal Methods - Getting IT Right, volume 2391 of Lecture Notes in Computer Science, pages 451-470. Springer-Verlag, unknown 2002.

    [29] G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in Systems Design, 18:249-284, May 2001.

    [30] J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 2nd edition, 1992.

  • Related Organizations (4)
  • Metrics
Share - Bookmark