SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications

Hugo Filipe Mendes Torres Vieira; Luís Manuel Marques da Costa Caires

doi:10.1007/978-3-642-28756-5_35

SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications

Hugo Filipe Mendes Torres Vieira, Luís Manuel Marques da Costa Caires

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

7 Citations (Scopus)

Abstract

The Spatial Logic Model Checker is a tool for verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic for concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques to check temporal properties of software systems. However, when the analysis focuses on properties related to resource usage, localities, interference, mobility, or topology, it is crucial to reason about spatial properties and structural dynamics. The SLMC is the only currently available tool that supports the combined analysis of behavioral and spatial properties of systems. The implementation, written in OCAML, is mature and robust, available in open source, and outperforms other tools for verifying systems modeled in the π-calculus.

Original language	Unknown
Title of host publication	Lecture Notes in Computer Science
Pages	485-491
DOIs	https://doi.org/10.1007/978-3-642-28756-5_35
Publication status	Published - 1 Jan 2012
Event	TACAS 2012 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Duration: 1 Jan 2012 → …

Conference

Conference	TACAS 2012 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Period	1/01/12 → …

Access to Document

10.1007/978-3-642-28756-5_35

Cite this

@inproceedings{497dacd476cd456a88c65cd704a1033e,

title = "SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications",

abstract = "The Spatial Logic Model Checker is a tool for verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic for concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques to check temporal properties of software systems. However, when the analysis focuses on properties related to resource usage, localities, interference, mobility, or topology, it is crucial to reason about spatial properties and structural dynamics. The SLMC is the only currently available tool that supports the combined analysis of behavioral and spatial properties of systems. The implementation, written in OCAML, is mature and robust, available in open source, and outperforms other tools for verifying systems modeled in the π-calculus.",

author = "Vieira, {Hugo Filipe Mendes Torres} and Caires, {Lu{\'i}s Manuel Marques da Costa}",

year = "2012",

month = jan,

day = "1",

doi = "10.1007/978-3-642-28756-5_35",

language = "Unknown",

isbn = "978-3-642-28755-8",

pages = "485--491",

booktitle = "Lecture Notes in Computer Science",

note = "TACAS 2012 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ; Conference date: 01-01-2012",

}

TY - GEN

T1 - SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications

AU - Vieira, Hugo Filipe Mendes Torres

AU - Caires, Luís Manuel Marques da Costa

PY - 2012/1/1

Y1 - 2012/1/1

N2 - The Spatial Logic Model Checker is a tool for verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic for concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques to check temporal properties of software systems. However, when the analysis focuses on properties related to resource usage, localities, interference, mobility, or topology, it is crucial to reason about spatial properties and structural dynamics. The SLMC is the only currently available tool that supports the combined analysis of behavioral and spatial properties of systems. The implementation, written in OCAML, is mature and robust, available in open source, and outperforms other tools for verifying systems modeled in the π-calculus.

AB - The Spatial Logic Model Checker is a tool for verifying π-calculus systems against safety, liveness, and structural properties expressed in the spatial logic for concurrency of Caires and Cardelli. Model-checking is one of the most widely used techniques to check temporal properties of software systems. However, when the analysis focuses on properties related to resource usage, localities, interference, mobility, or topology, it is crucial to reason about spatial properties and structural dynamics. The SLMC is the only currently available tool that supports the combined analysis of behavioral and spatial properties of systems. The implementation, written in OCAML, is mature and robust, available in open source, and outperforms other tools for verifying systems modeled in the π-calculus.

U2 - 10.1007/978-3-642-28756-5_35

DO - 10.1007/978-3-642-28756-5_35

M3 - Conference contribution

SN - 978-3-642-28755-8

SP - 485

EP - 491

BT - Lecture Notes in Computer Science

T2 - TACAS 2012 - 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Y2 - 1 January 2012

ER -