An abstract interpretation toolkit for μCRL

Miguel Valero Espada, Jaco van de Pol

Research output: Contribution to journalArticleAcademicpeer-review

5 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)249-273
Number of pages25
JournalFormal methods in system design
Volume30
Issue number3
DOIs
Publication statusPublished - Jun 2007

Fingerprint

Abstract Interpretation
Labels
Algebraic Specification
Specifications
Labeled Transition System
Liveness
Transition Systems
Tool Support
Modality
Branching
Calculus
Safety
Approximation
Abstraction
Language

Keywords

  • FMT-MC: MODEL CHECKING
  • Model checking
  • Process algebra
  • μCRL
  • Abstract interpretation

Cite this

Valero Espada, Miguel ; van de Pol, Jaco. / An abstract interpretation toolkit for μCRL. In: Formal methods in system design. 2007 ; Vol. 30, No. 3. pp. 249-273.
@article{30009c7515b94bac890d44b026269b88,
title = "An abstract interpretation toolkit for μCRL",
abstract = "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.",
keywords = "FMT-MC: MODEL CHECKING, Model checking, Process algebra, μCRL, Abstract interpretation",
author = "{Valero Espada}, Miguel and {van de Pol}, Jaco",
year = "2007",
month = "6",
doi = "10.1007/s10703-006-0029-7",
language = "English",
volume = "30",
pages = "249--273",
journal = "Formal methods in system design",
issn = "0925-9856",
publisher = "Springer",
number = "3",

}

An abstract interpretation toolkit for μCRL. / Valero Espada, Miguel; van de Pol, Jaco.

In: Formal methods in system design, Vol. 30, No. 3, 06.2007, p. 249-273.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - An abstract interpretation toolkit for μCRL

AU - Valero Espada, Miguel

AU - van de Pol, Jaco

PY - 2007/6

Y1 - 2007/6

N2 - 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.

AB - 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.

KW - FMT-MC: MODEL CHECKING

KW - Model checking

KW - Process algebra

KW - μCRL

KW - Abstract interpretation

U2 - 10.1007/s10703-006-0029-7

DO - 10.1007/s10703-006-0029-7

M3 - Article

VL - 30

SP - 249

EP - 273

JO - Formal methods in system design

JF - Formal methods in system design

SN - 0925-9856

IS - 3

ER -