Compositional Abstraction of CSPZ Processes

Adalberto FariasAlexandre Cabral MotaAugusto Sampaio

Data abstraction is a powerful technique to overcomestate explosion in model checking. For CSPZ (a formal integrationof the well-known specification languages CSPand Z), current approaches can mechanically abstract infinitedomains (types) as long as they are not used incommunications. This work presents a compositional andsystematic approach to data abstract CSPZ specificationseven when communications are based on infinite domains.Therefore, we deal with a larger class of specificationsthan the previous techniques. Our approach requires thatthe domains (used in communications) being abstracteddo not affect the behaviour of the system (data independence).This criteria is used to achieve an internal partitioningof the specification in such a way that complementarytechniques for abstracting data types can be appliedto the components of the partition. Afterwards, the partialresults can be compositionally combined to abstractthe entire specification. We propose an algorithm that implementsthe partitioning and show the application of theentire approach to a real case study.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: