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
Publisher: Springer
Languages: English
Types: Unknown
Subjects: QA76
Data refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements, which can be checked on an event-by-event basis rather than per trace. In models of concurrency, refinement is often defined in terms of sets of observations, which can include the events a system is prepared to accept or refuse, or depend on explicit properties of states and transitions. By embedding such concurrent semantics into a relational one, eventwise verification methods for such refinement relations can be derived. In this paper we continue our program of deriving simulation conditions for process algebraic refinement by considering how notions of time should be embedded into a relational model, and thereby deriving relational notions of timed refinement.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. J. A. Bergstra, A. Ponse, and Scott A. Smolka, editors. Handbook of Process Algebra. Elsevier Science Inc., New York, NY, USA, 2001.
    • 2. E.A. Boiten and J. Derrick. Modelling divergence in relational concurrent refinement. In M. Leuschel and H. Wehrheim, editors, IFM 2009: Integrated Formal Methods, volume 5423 of LNCS, pages 183-199. Springer Verlag, February 2009.
    • 3. E.A. Boiten, J. Derrick, and G. Schellhorn. Relational concurrent refinement II: Internal operations and outputs. Formal Aspects of Computing, 21(1-2):65-102, 2009.
    • 4. W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. CUP, 1998.
    • 5. J. Derrick and E. A. Boiten. Refinement in Z and Object-Z. Springer-Verlag, 2001.
    • 6. J. Derrick and E.A. Boiten. Relational concurrent refinement. Formal Aspects of Computing, 15(1):182-214, November 2003.
    • 7. J. Derrick and E.A. Boiten. More relational refinement: traces and partial relations. Electronic Notes in Theoretical Computer Science, 214:255-276, May 2008. Proceedings of REFINE 2008 (Turku, May 2008).
    • 8. John Derrick and Eerke Boiten. Relational concurrent refinement: Automata. Electronic Notes in Theoretical Computer Science, 259:21-34, December 2009. Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009). Extended version “Relational Concurrent Refinement III” submitted to Formal Aspects of Computing.
    • 9. He Jifeng and C. A. R. Hoare. Prespecification and data refinement. In Data Refinement in a Categorical Setting, Technical Monograph, number PRG-90. Oxford University Computing Laboratory, November 1990.
    • 10. He Jifeng, C. A. R. Hoare, and J. W. Sanders. Data refinement refined. In B. Robinet and R. Wilhelm, editors, Proc. ESOP 86, volume 213 of Lecture Notes in Computer Science, pages 187-196. Springer-Verlag, 1986.
    • 11. C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
    • 12. Nancy Lynch and Frits Vaandrager. Forward and backward simulations I.: untimed systems. Information and Computation, 121(2):214-233, 1995.
    • 13. Nancy Lynch and Frits Vaandrager. Forward and backward simulations Part II: timingbased systems. Information and Computation, 128(1):1-25, 1996.
    • 14. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
    • 15. M. W. Mislove, A. W. Roscoe, and S. A. Schneider. Fixed points without completeness. Theoretical Computer Science, 138(2):273-314, 1995.
    • 16. Xavier Nicollin and Joseph Sifakis. An overview and synthesis on timed process algebras. In Proceedings of the Real-Time: Theory in Practice, REX Workshop, pages 526-548, London, UK, 1992. Springer-Verlag.
    • 17. G. M. Reed and A. W. Roscoe. A timed model for communicating sequential processes. Theor. Comput. Sci., 58(1-3):249-261, 1988.
    • 18. G. M. Reed and A. W. Roscoe. The timed failures-stability model for CSP. Theoretical Computer Science, 211(1-2):85-127, 1999.
    • 19. George M. Reed. A uniform mathematical theory for real-time distributed computing. PhD thesis, 1988.
    • 20. George M. Reed and A. W. Roscoe. A timed model for communicating sequential processes. In Laurent Kott, editor, ICALP, volume 226 of Lecture Notes in Computer Science, pages 314-323. Springer, 1986.
    • 21. Steve Schneider. Timewise refinement for communicating processes. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pages 177-214, London, UK, 1994. Springer-Verlag.
    • 22. Steve Schneider. Timewise refinement for communicating processes. Sci. Comput. Program., 28(1):43-90, 1997.
    • 23. Steve Schneider. Concurrent and Real Time Systems: The CSP Approach. John Wiley & Sons, Inc., New York, NY, USA, 1999.
    • 24. R. J. van Glabbeek. The linear time - branching time spectrum I. The semantics of concrete sequential processes. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland, 2001.
    • 25. R.J. van Glabbeek. The linear time - branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract).
    • 26. J. C. P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article