Blog
About

161
views
0
recommends
+1 Recommend
1 collections
    3
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Using Temporal Fixpoints to Compositionally Reason about Liveness

      Proceedings of the BCS-FACS 7th Refinement Workshop (RW)

      BCS-FACS 7th Refinement Workshop

      3-5 July 1996

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          The compositional specification and verification of the behavior of concurrent processes is a challenging research area. The assumption/commitment approach has emerged as oneway to systematically achieve the desiredmodularity. However, it is generally limited to reasoning about safety propertieswhich apply throughout the execution of a system. Liveness properties involving intermittent behavior are harder to address. We investigate the use of assumptions and commitments in Interval Temporal Logic and show how to augment them with some more information for handling liveness. The proposed techniques are a continuation of our previous research on formalizing assumptions and commitments through the use of fixpoints of certain simple temporal operators. Associated with this is a generalized notion of Owicki and Gries’ proof outlines. We illustrate the approach with examples including a mutual exclusion system with time stamps.

          Related collections

          Most cited references 3

          • Record: found
          • Abstract: not found
          • Article: not found

          An axiomatic proof technique for parallel programs I

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            P — A logic — a compositional proof system for distributed programs

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Proving Total Correctness with Respect to a Fair (Shared-State) Parallel Language

               Ketil Stølen (1992)
                Bookmark

                Author and article information

                Conference
                July 1996
                July 1996
                : 1-28
                Affiliations
                Department of Electrical and Electronic Engineering

                University of Newcastle upon Tyne, Newcastle NE1 7RU, Great Britain
                Article
                10.14236/ewic/RW1996.11
                © Ben Moszkowski. Published by BCS Learning and Development Ltd. Proceedings of the BCS-FACS 7th Refinement Workshop, Bath

                This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

                Proceedings of the BCS-FACS 7th Refinement Workshop
                RW
                7
                Bath
                3-5 July 1996
                Electronic Workshops in Computing (eWiC)
                BCS-FACS 7th Refinement Workshop
                Product
                Product Information: 1477-9358BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Categories
                Electronic Workshops in Computing

                Comments

                Comment on this article