30
views
0
recommends
+1 Recommend
1 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Compositional abstraction of CSP Z processes

      research-article

      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

          Data abstraction is a powerful technique to overcome state explosion in model checking. For CSP Z (a formal integration of the well-known specification languages CSP and Z), current approaches can mechanically abstract infinite domains (types) as long as they are not used in communications. This work presents a compositional and systematic approach to data abstract CSP Z specifications even when communications are based on infinite domains. Therefore, we deal with a larger class of specifications than the previous techniques. Our approach requires that the domains (used in communications) being abstracted do not affect the behaviour of the system (data independence). This criteria is used to achieve an internal partitioning of the specification in such a way that complementary techniques for abstracting data types can be applied to the components of the partition. Afterwards, the partial results can be compositionally combined to abstract the entire specification. We propose an algorithm that implements the partitioning and show the application of the entire approach to a real case study.

          Related collections

          Most cited references19

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

          Abstract Interpretation Frameworks

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

            The theory and practice of concurrency

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

              Compilers: Principles, Techniques and Tools

                Bookmark

                Author and article information

                Contributors
                Role: ND
                Role: ND
                Role: ND
                Journal
                jbcos
                Journal of the Brazilian Computer Society
                J. Braz. Comp. Soc.
                Sociedade Brasileira de Computação (Campinas )
                1678-4804
                2008
                : 14
                : 2
                : 23-44
                Affiliations
                [1 ] Universidade Federal de Pernambuco Brazil
                Article
                S0104-65002008000200003
                10.1590/S0104-65002008000200003
                f532d4f5-35fa-4593-9b57-65c53552bd0f

                http://creativecommons.org/licenses/by/4.0/

                History
                Product

                SciELO Brazil

                Self URI (journal page): http://www.scielo.br/scielo.php?script=sci_serial&pid=0104-6500&lng=en
                Categories
                COMPUTER SCIENCE, INFORMATION SYSTEMS

                Information systems & theory
                Formal Methods,Model Checking,Data Abstraction,CSP,Z,Compositionality
                Information systems & theory
                Formal Methods, Model Checking, Data Abstraction, CSP, Z, Compositionality

                Comments

                Comment on this article