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

      On the Automatic Verification of Non-Standard Measures of Consistency

      ,

      6th International Workshop on Formal Methods (FM)

      Formal Methods

      11 July 2003

      Refinement, formal verification techniques, model-checking, CSP

      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

          Consistency between a process and its specification expressed in CSP is typically presented as a refinement check. Within the traces model consistency is measured by examining only the traces of the systems, whilst in the finer stable failures model the possibility of subsequently refusing a combination of events is also taken into consideration.

          The contribution of this paper is to identify and motivate the need for alternative measures of consistency, and to present and prove the soundness and completeness of general techniques for automatically verifying such consistencies. We achieve this by masking all failures information other than that associated with the measure in question.

          More concretely, we describe methods for automatically checking: that a process can refuse a given set of events after any trace only if its specification can refuse the same set of events after the same trace; that a process might deadlock after any trace only if its specification might also deadlock after the same trace; and that a process might after any trace refuse a given number of events of a particular class only if its specification might also refuse the same set after the same trace.

          Related collections

          Most cited references 2

          • Record: found
          • Abstract: not found
          • Conference Proceedings: not found

          The temporal logic of programs

           Amir Pnueli (1977)
            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Combining Independent Specifications

              Bookmark

              Author and article information

              Contributors
              Conference
              July 2003
              July 2003
              : 1-15
              Affiliations
              Oxford University Computing Laboratory

              Wolfson Building, Parks Road

              Oxford OX1 3QD, England
              Article
              10.14236/ewic/IWFM2003.5
              © Christie Bolton et al. Published by BCS Learning and Development Ltd. 6th International Workshop on Formal Methods, Dublin City University, Ireland

              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/

              6th International Workshop on Formal Methods
              FM
              6
              Dublin City University, Ireland
              11 July 2003
              Electronic Workshops in Computing (eWiC)
              Formal Methods
              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