Compositional abstraction of CSP Z processes
AUTOR(ES)
Farias, Adalberto, Mota, Alexandre, Sampaio, Augusto
FONTE
Journal of the Brazilian Computer Society
DATA DE PUBLICAÇÃO
2008
RESUMO
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.
Documentos Relacionados
- Abstraction of infinite and communicating CSPZ processes
- Villa-Lobos compositional processes, a theoretic guide
- Compositional compartmentalization and compositional patterns in the nuclear genomes of plants.
- The B- to Z-DNA equilibrium in vivo is perturbed by biological processes.
- Processos de composição microtonal por meio do modelo de dissonancia sensorial