Tampere University of Technology

TUTCRIS Research Portal

A State Space Tool for Concurrent System Models Expressed In C++

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Details

Original languageEnglish
Title of host publicationSPLST 2015 Symposium on Programming Languages and Software Tools
Subtitle of host publicationProceedings of the 14th Symposium on Programming Languages and Software Tools (SPLST'15) Tampere, Finland, Oct 9-10, 2015
EditorsJyrki Nummenmaa, Outi Sievi-Korte, Erkki Mäkinen
PublisherCEUR-WS.org
Pages91-105
Number of pages15
Volume1525
Publication statusPublished - 14 Dec 2015
Publication typeA4 Article in a conference publication
EventSymposium on Programming Languages and Software Tools -
Duration: 1 Jan 1900 → …

Publication series

NameCEUR Workshop Proceedings
Volume1525
ISSN (Electronic)1613-0073

Conference

ConferenceSymposium on Programming Languages and Software Tools
Period1/01/00 → …

Abstract

This publication introduces a state space exploration tool that is based on representing the model under verification as a piece of C++ code that obeys certain conventions. This approach facilitates experimenting with many kinds of modelling ideas. On the other hand, the use of stubborn sets and symmetries requires that either the modeller or a preprocessor tool analyses the model at a syntactic level and expresses stubborn set obligation rules and the symmetry mapping as suitable C++ functions. The tool supports the detection of illegal deadlocks, safety errors, and may progress errors. It also partially supports the detection of must progress errors.

ASJC Scopus subject areas

Keywords

  • model checking; stubborn sets; symmetries; safety; progress

Publication forum classification

Field of science, Statistics Finland