Multi-Core LTSmin: Marrying Modularity and Scalability

Alfons Laarman, Jan Cornelis van de Pol, M. Weber

  • 26 Citations

Abstract

The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.
Original languageUndefined
Title of host publicationProceedings of the Third International Symposium on NASA Formal Methods, NFM 2011
EditorsMichaela Bobaru, Klaus Havelund, Gerard J. Holzmann, Rajeev Joshi
Place of PublicationBerlin
PublisherSpringer Verlag
Pages506-511
Number of pages6
ISBN (Print)978-3-642-20397-8
DOIs
StatePublished - Jul 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6617
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Model checking
Resource allocation
Specifications

Keywords

  • METIS-277604
  • IR-77023
  • tree-based algorithm
  • compression
  • EWI-20004
  • Parallel
  • Multi-Core
  • Model Checking
  • FMT-MC: MODEL CHECKING
  • incremental hashing

Cite this

Laarman, A., van de Pol, J. C., & Weber, M. (2011). Multi-Core LTSmin: Marrying Modularity and Scalability. In M. Bobaru, K. Havelund, G. J. Holzmann, & R. Joshi (Eds.), Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011 (pp. 506-511). (Lecture Notes in Computer Science; Vol. 6617). Berlin: Springer Verlag. DOI: 10.1007/978-3-642-20398-5_40

Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M. / Multi-Core LTSmin: Marrying Modularity and Scalability.

Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. ed. / Michaela Bobaru; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi. Berlin : Springer Verlag, 2011. p. 506-511 (Lecture Notes in Computer Science; Vol. 6617).

Research output: Scientific - peer-reviewConference contribution

@inbook{9c01a0988d65427cbfc58f9565899e70,
title = "Multi-Core LTSmin: Marrying Modularity and Scalability",
abstract = "The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.",
keywords = "METIS-277604, IR-77023, tree-based algorithm, compression, EWI-20004, Parallel, Multi-Core, Model Checking, FMT-MC: MODEL CHECKING, incremental hashing",
author = "Alfons Laarman and {van de Pol}, {Jan Cornelis} and M. Weber",
note = "10.1007/978-3-642-20398-5_40",
year = "2011",
month = "7",
doi = "10.1007/978-3-642-20398-5_40",
isbn = "978-3-642-20397-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "506--511",
editor = "Michaela Bobaru and Klaus Havelund and Holzmann, {Gerard J.} and Rajeev Joshi",
booktitle = "Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011",

}

Laarman, A, van de Pol, JC & Weber, M 2011, Multi-Core LTSmin: Marrying Modularity and Scalability. in M Bobaru, K Havelund, GJ Holzmann & R Joshi (eds), Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. Lecture Notes in Computer Science, vol. 6617, Springer Verlag, Berlin, pp. 506-511. DOI: 10.1007/978-3-642-20398-5_40

Multi-Core LTSmin: Marrying Modularity and Scalability. / Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M.

Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. ed. / Michaela Bobaru; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi. Berlin : Springer Verlag, 2011. p. 506-511 (Lecture Notes in Computer Science; Vol. 6617).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Multi-Core LTSmin: Marrying Modularity and Scalability

AU - Laarman,Alfons

AU - van de Pol,Jan Cornelis

AU - Weber,M.

N1 - 10.1007/978-3-642-20398-5_40

PY - 2011/7

Y1 - 2011/7

N2 - The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.

AB - The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed model checking algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.

KW - METIS-277604

KW - IR-77023

KW - tree-based algorithm

KW - compression

KW - EWI-20004

KW - Parallel

KW - Multi-Core

KW - Model Checking

KW - FMT-MC: MODEL CHECKING

KW - incremental hashing

U2 - 10.1007/978-3-642-20398-5_40

DO - 10.1007/978-3-642-20398-5_40

M3 - Conference contribution

SN - 978-3-642-20397-8

T3 - Lecture Notes in Computer Science

SP - 506

EP - 511

BT - Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011

PB - Springer Verlag

ER -

Laarman A, van de Pol JC, Weber M. Multi-Core LTSmin: Marrying Modularity and Scalability. In Bobaru M, Havelund K, Holzmann GJ, Joshi R, editors, Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011. Berlin: Springer Verlag. 2011. p. 506-511. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-20398-5_40