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, and the other focus on the behavioural aspects of the system. Some combined languages have already been proposed to bring these two schools together. However, as far as we know, none of them has a related refinement calculus. Using Circus as the specification language, we can describe both data and control behaviour. The objective of this work is to formalise a refinement calculus for Circus. A refinement strategy for Circus, new refinement laws and their proofs are presented. The proofs are based on an extension of the existing Circus semantics, which is based on the unifying theory of programming. This extension, and its mechanisation, and the proof of the laws on ProofPower are also part of this work. We intend to provide a tool that supports the Circus refinement calculus. Furthermore, as an extension of the existing refinement strategy for Circus, we present a translation strategy for Circus programs. This translation strategy can be used as a guideline in the translation of Circus programs to Java. Furthermore, the mechanisation of this translation is also feasible. We present a case study, a safety-critical fire protection system, that, as far as we know, is the largest case study on the Circus refinement calculus. We present the refinement of its abstract centralised specification to a concrete distributed one. Finally, the translation of the concrete specification of the system to Java, using our translation strategy, is also presented. Throughout this mini-thesis, some sections, and even chapters are not written. They have not been removed from the mini-thesis on purpose. Our intention is to give an idea of the scope and the structure of our final thesis, which is discussed in details in the final chapter of this document.
  • 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.

  • Metrics
    0
    views in OpenAIRE
    0
    views in local repository
    2
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Kent Academic Repository - IRUS-UK 0 2
Share - Bookmark