An abstract interpretation toolkit for μCRL

被引：0

作者：

Miguel Valero Espada

Jaco van de Pol

机构：

[1] Universidad Complutense de Madrid,Dept. de Sistemas Informáticos y Programación

[2] Centrum voor Wiskunde en Informatica,undefined

来源：

Formal Methods in System Design | 2007年 / 30卷

关键词：

Model checking; Process algebra; muCRL; Abstract interpretation;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

This paper describes a toolkit that assists in the task of generating abstract approximations of process algebraic specifications written in the language μCRL. Abstractions are represented by Modal Labelled Transition Systems, which are mixed transition systems with may and must modalities. The approach permits to infer the satisfaction or refutation of safety and liveness properties expressed in the (action-based) μ-calculus. The tool supports the abstraction of states and action labels, which allows to deal with infinitely branching systems.

引用

页码：249 / 273

页数：24

共 16 条

[1] Bergstra JA(1985)Algebra of communicating processes with abstraction Theor Comput Sci 37 77-121
[2] Klop JW(2004)αSPIN: a tool for abstract model checking Int J Softw Tools for Technol Transf (STTT) 5 165-184
[3] Gallardo MM(2002)An overview of CADP 2001 Eur Assoc Softw Sci Technol Newsl 4 13-24
[4] Martínez J(2001)Linearization in parallel pCRL J Logic Algebraic Programm 48 39-70
[5] Merino P(1944)Galois connexions Trans. Am Math Soc 55 493-513
[6] Pimentel E(2005)A state space distribution policy based on abstract interpretation ENTCS 128 35-45
[7] Garavel H(undefined)undefined undefined undefined undefined-undefined
[8] Lang F(undefined)undefined undefined undefined undefined-undefined
[9] Mateescu R(undefined)undefined undefined undefined undefined-undefined
[10] Groote JF(undefined)undefined undefined undefined undefined-undefined

← 1 2 →