mctau: Bridging the Gap between Modest and UPPAAL

Jonathan Bogdoll; Alexandre David; Arnd Harmanns; Holger Hermanns

doi:10.1007/978-3-642-31759-0_16

mctau: Bridging the Gap between Modest and UPPAAL

Jonathan Bogdoll, Alexandre David, Arnd Harmanns, Holger Hermanns

Institut for Datalogi

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

7 Citationer (Scopus)

Abstract

Modest is a high-level compositional modelling language for stochastic timed systems with a formal semantics in terms of stochastic timed automata, an overarching formalism of which several well-studied models are special cases. The emphasis of Modest is to make use of existing analysis techniques and tools in a single-formalism, multiple-solution approach. In this paper, we focus on networks of timed automata as supported by Uppaal. We report on extensions made to Modest and Uppaal that allow the transformation of a rich subset of Modest models to Uppaal timed automata and enable connections to further tools and formalisms. We present our Modest-to-Uppaal tool chain mctau, which allows both a fully automated analysis as well as model transformation, and we compare its performance with the existing mcpta tool.

Originalsprog	Engelsk
Titel	Model Checking Software : 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings
Redaktører	Alastair Donaldson, David Parker
Antal sider	7
Vol/bind	7385
Udgivelsessted	Berlin
Forlag	Springer
Publikationsdato	2012
Sider	227-233
ISBN (Trykt)	978-3-642-31758-3
ISBN (Elektronisk)	978-3-642-31759-0
DOI	https://doi.org/10.1007/978-3-642-31759-0_16
Status	Udgivet - 2012
Begivenhed	19th International Workshop, SPIN 2012 - Oxford, Storbritannien Varighed: 23 jul. 2012 → 24 jul. 2012 Konferencens nummer: 19th

Konference

Konference	19th International Workshop, SPIN 2012
Nummer	19th
Land/Område	Storbritannien
By	Oxford
Periode	23/07/2012 → 24/07/2012

Navn	Lecture Notes in Computer Science (LNCS)
Vol/bind	7385
ISSN	0302-9743

Adgang til dokumentet

10.1007/978-3-642-31759-0_16

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

Link to publication in Scopus

Citationsformater

@inproceedings{5267d9a84ea04e419bb18fe0355a2632,

title = "mctau: Bridging the Gap between Modest and UPPAAL",

abstract = "Modest is a high-level compositional modelling language for stochastic timed systems with a formal semantics in terms of stochastic timed automata, an overarching formalism of which several well-studied models are special cases. The emphasis of Modest is to make use of existing analysis techniques and tools in a single-formalism, multiple-solution approach. In this paper, we focus on networks of timed automata as supported by Uppaal. We report on extensions made to Modest and Uppaal that allow the transformation of a rich subset of Modest models to Uppaal timed automata and enable connections to further tools and formalisms. We present our Modest-to-Uppaal tool chain mctau, which allows both a fully automated analysis as well as model transformation, and we compare its performance with the existing mcpta tool. ",

author = "Jonathan Bogdoll and Alexandre David and Arnd Harmanns and Holger Hermanns",

year = "2012",

doi = "10.1007/978-3-642-31759-0_16",

language = "English",

isbn = "978-3-642-31758-3",

volume = "7385",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "227--233",

editor = "Alastair Donaldson and Parker, {David }",

booktitle = "Model Checking Software",

address = "Germany",

note = "19th International Workshop, SPIN 2012 ; Conference date: 23-07-2012 Through 24-07-2012",

}

Bogdoll, J, David, A, Harmanns, A & Hermanns, H 2012, mctau: Bridging the Gap between Modest and UPPAAL. i A Donaldson & D Parker (red), Model Checking Software: 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. bind 7385, Springer, Berlin, Lecture Notes in Computer Science (LNCS), bind 7385, s. 227-233, 19th International Workshop, SPIN 2012, Oxford, Storbritannien, 23/07/2012. https://doi.org/10.1007/978-3-642-31759-0_16

mctau: Bridging the Gap between Modest and UPPAAL. / Bogdoll, Jonathan; David, Alexandre; Harmanns, Arnd et al.
Model Checking Software: 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. red. / Alastair Donaldson; David Parker. Bind 7385 Berlin: Springer, 2012. s. 227-233 (Lecture Notes in Computer Science (LNCS), Bind 7385).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

TY - GEN

T1 - mctau

T2 - 19th International Workshop, SPIN 2012

AU - Bogdoll, Jonathan

AU - David, Alexandre

AU - Harmanns, Arnd

AU - Hermanns, Holger

N1 - Conference code: 19th

PY - 2012

Y1 - 2012

N2 - Modest is a high-level compositional modelling language for stochastic timed systems with a formal semantics in terms of stochastic timed automata, an overarching formalism of which several well-studied models are special cases. The emphasis of Modest is to make use of existing analysis techniques and tools in a single-formalism, multiple-solution approach. In this paper, we focus on networks of timed automata as supported by Uppaal. We report on extensions made to Modest and Uppaal that allow the transformation of a rich subset of Modest models to Uppaal timed automata and enable connections to further tools and formalisms. We present our Modest-to-Uppaal tool chain mctau, which allows both a fully automated analysis as well as model transformation, and we compare its performance with the existing mcpta tool.

AB - Modest is a high-level compositional modelling language for stochastic timed systems with a formal semantics in terms of stochastic timed automata, an overarching formalism of which several well-studied models are special cases. The emphasis of Modest is to make use of existing analysis techniques and tools in a single-formalism, multiple-solution approach. In this paper, we focus on networks of timed automata as supported by Uppaal. We report on extensions made to Modest and Uppaal that allow the transformation of a rich subset of Modest models to Uppaal timed automata and enable connections to further tools and formalisms. We present our Modest-to-Uppaal tool chain mctau, which allows both a fully automated analysis as well as model transformation, and we compare its performance with the existing mcpta tool.

UR - http://www.scopus.com/inward/record.url?scp=84864862310&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-31759-0_16

DO - 10.1007/978-3-642-31759-0_16

M3 - Article in proceeding

SN - 978-3-642-31758-3

VL - 7385

T3 - Lecture Notes in Computer Science (LNCS)

SP - 227

EP - 233

BT - Model Checking Software

A2 - Donaldson, Alastair

A2 - Parker, David

PB - Springer

CY - Berlin

Y2 - 23 July 2012 through 24 July 2012

ER -

Bogdoll J, David A, Harmanns A, Hermanns H. mctau: Bridging the Gap between Modest and UPPAAL. I Donaldson A, Parker D, red., Model Checking Software: 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. Bind 7385. Berlin: Springer. 2012. s. 227-233. (Lecture Notes in Computer Science (LNCS), Bind 7385). doi: 10.1007/978-3-642-31759-0_16

mctau: Bridging the Gap between Modest and UPPAAL

Abstract

Konference

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Citationsformater