Compositional abstraction of CSP Z processes

Journal of the Brazilian Computer Society

Federal University of Pernambuco, Recife, BRAZIL¹  Mota, Alexandre¹  Farias, Adalberto¹  Sampaio, Augusto¹ 

关键词: Formal Methods;    Model Checking;    Data Abstraction;    CSP;    Z;    Compositionality.;   

DOI  :  10.1007/BF03192557

学科分类：农业科学（综合）

来源: Springer U K

【 摘 要 】

Data abstraction is a powerful technique to overcome state explosion in model checking. For CSPZ (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 CSPZ 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.

【 授权许可】

Unknown