LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Oliveira, Marcel V. M. (2004)
Publisher: University of Kent
Languages: English
Types: Book
Subjects: QA76

Classified by OpenAIRE into

ACM Ref: 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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 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.
  • No related research data.
  • No similar publications.

Share - Bookmark

Download from

Cite this article