JANI: Quantitative Model and Tool Interaction

Carlos E. Budde; Christian Dehnert; Ernst Moritz Hahn; Arnd Hartmanns; Sebastian Junges; Andrea Turrini

doi:10.1007/978-3-662-54580-5_9

JANI: Quantitative Model and Tool Interaction

Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini

University of Twente

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

57 Citations (Scopus)

24 Downloads (Pure)

Abstract

The formal analysis of critical systems is supported by a vast space of modelling formalisms and tools. The variety of incompatible formats and tools however poses a significant challenge to practical adoption as well as continued research. In this paper, we propose the Jani model format and tool interaction protocol. The format is a metamodel based on networks of communicating automata and has been designed for ease of implementation without sacrificing readability. The purpose of the protocol is to provide a stable and uniform interface between tools such as model checkers, transformers, and user interfaces. Jani uses the Json data format, inheriting its ease of use and inherent extensibility. Jani initially targets, but is not limited to, quantitative model checking. Several existing tools now support the verification of Jani models, and automatic converters from a diverse set of higher-level modelling languages have been implemented. The ultimate purpose of Jani is to simplify tool development, encourage research cooperation, and pave the way towards a future competition in quantitative model checking.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings
Editors	Axel Legay, Tiziana Margaria
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	151-168
Number of pages	18
Volume	Part II
ISBN (Electronic)	978-3-662-54576-8
ISBN (Print)	978-3-662-54579-9
DOIs	https://doi.org/10.1007/978-3-662-54580-5_9
Publication status	Published - 2017
Event	23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 - Uppsala, Sweden Duration: 22 Apr 2017 → 29 Apr 2017 Conference number: 23

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10206
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017
Abbreviated title	TACAS
Country/Territory	Sweden
City	Uppsala
Period	22/04/17 → 29/04/17

Keywords

Janis model
Quantitative model checking
Inherent extensibility
Probabilistic Computation Tree Logic (PCTL)
Modest toolset

Access to Document

10.1007/978-3-662-54580-5_9

Cite this

Budde, C. E., Dehnert, C., Hahn, E. M., Hartmanns, A., Junges, S., & Turrini, A. (2017). JANI: Quantitative Model and Tool Interaction. In A. Legay, & T. Margaria (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Vol. Part II, pp. 151-168). (Lecture Notes in Computer Science; Vol. 10206). Springer. https://doi.org/10.1007/978-3-662-54580-5_9

Budde, Carlos E. ; Dehnert, Christian ; Hahn, Ernst Moritz et al. / JANI: Quantitative Model and Tool Interaction. Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. editor / Axel Legay ; Tiziana Margaria. Vol. Part II Berlin, Heidelberg : Springer, 2017. pp. 151-168 (Lecture Notes in Computer Science).

@inproceedings{a005cf657cf7491693f8654f6b0a76c4,

title = "JANI: Quantitative Model and Tool Interaction",

abstract = "The formal analysis of critical systems is supported by a vast space of modelling formalisms and tools. The variety of incompatible formats and tools however poses a significant challenge to practical adoption as well as continued research. In this paper, we propose the Jani model format and tool interaction protocol. The format is a metamodel based on networks of communicating automata and has been designed for ease of implementation without sacrificing readability. The purpose of the protocol is to provide a stable and uniform interface between tools such as model checkers, transformers, and user interfaces. Jani uses the Json data format, inheriting its ease of use and inherent extensibility. Jani initially targets, but is not limited to, quantitative model checking. Several existing tools now support the verification of Jani models, and automatic converters from a diverse set of higher-level modelling languages have been implemented. The ultimate purpose of Jani is to simplify tool development, encourage research cooperation, and pave the way towards a future competition in quantitative model checking.",

keywords = "Janis model, Quantitative model checking, Inherent extensibility, Probabilistic Computation Tree Logic (PCTL), Modest toolset",

author = "Budde, {Carlos E.} and Christian Dehnert and Hahn, {Ernst Moritz} and Arnd Hartmanns and Sebastian Junges and Andrea Turrini",

year = "2017",

doi = "10.1007/978-3-662-54580-5_9",

language = "English",

isbn = "978-3-662-54579-9",

volume = "Part II",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "151--168",

editor = "Axel Legay and Tiziana Margaria",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, TACAS ; Conference date: 22-04-2017 Through 29-04-2017",

}

Budde, CE, Dehnert, C, Hahn, EM, Hartmanns, A, Junges, S & Turrini, A 2017, JANI: Quantitative Model and Tool Interaction. in A Legay & T Margaria (eds), Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. vol. Part II, Lecture Notes in Computer Science, vol. 10206, Springer, Berlin, Heidelberg, pp. 151-168, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, Uppsala, Sweden, 22/04/17. https://doi.org/10.1007/978-3-662-54580-5_9

JANI: Quantitative Model and Tool Interaction. / Budde, Carlos E.; Dehnert, Christian; Hahn, Ernst Moritz et al.
Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. ed. / Axel Legay; Tiziana Margaria. Vol. Part II Berlin, Heidelberg: Springer, 2017. p. 151-168 (Lecture Notes in Computer Science; Vol. 10206).

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

TY - GEN

T1 - JANI: Quantitative Model and Tool Interaction

AU - Budde, Carlos E.

AU - Dehnert, Christian

AU - Hahn, Ernst Moritz

AU - Hartmanns, Arnd

AU - Junges, Sebastian

AU - Turrini, Andrea

N1 - Conference code: 23

PY - 2017

Y1 - 2017

N2 - The formal analysis of critical systems is supported by a vast space of modelling formalisms and tools. The variety of incompatible formats and tools however poses a significant challenge to practical adoption as well as continued research. In this paper, we propose the Jani model format and tool interaction protocol. The format is a metamodel based on networks of communicating automata and has been designed for ease of implementation without sacrificing readability. The purpose of the protocol is to provide a stable and uniform interface between tools such as model checkers, transformers, and user interfaces. Jani uses the Json data format, inheriting its ease of use and inherent extensibility. Jani initially targets, but is not limited to, quantitative model checking. Several existing tools now support the verification of Jani models, and automatic converters from a diverse set of higher-level modelling languages have been implemented. The ultimate purpose of Jani is to simplify tool development, encourage research cooperation, and pave the way towards a future competition in quantitative model checking.

AB - The formal analysis of critical systems is supported by a vast space of modelling formalisms and tools. The variety of incompatible formats and tools however poses a significant challenge to practical adoption as well as continued research. In this paper, we propose the Jani model format and tool interaction protocol. The format is a metamodel based on networks of communicating automata and has been designed for ease of implementation without sacrificing readability. The purpose of the protocol is to provide a stable and uniform interface between tools such as model checkers, transformers, and user interfaces. Jani uses the Json data format, inheriting its ease of use and inherent extensibility. Jani initially targets, but is not limited to, quantitative model checking. Several existing tools now support the verification of Jani models, and automatic converters from a diverse set of higher-level modelling languages have been implemented. The ultimate purpose of Jani is to simplify tool development, encourage research cooperation, and pave the way towards a future competition in quantitative model checking.

KW - Janis model

KW - Quantitative model checking

KW - Inherent extensibility

KW - Probabilistic Computation Tree Logic (PCTL)

KW - Modest toolset

U2 - 10.1007/978-3-662-54580-5_9

DO - 10.1007/978-3-662-54580-5_9

M3 - Conference contribution

SN - 978-3-662-54579-9

VL - Part II

T3 - Lecture Notes in Computer Science

SP - 151

EP - 168

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Legay, Axel

A2 - Margaria, Tiziana

PB - Springer

CY - Berlin, Heidelberg

T2 - 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017

Y2 - 22 April 2017 through 29 April 2017

ER -

Budde CE, Dehnert C, Hahn EM, Hartmanns A, Junges S, Turrini A. JANI: Quantitative Model and Tool Interaction. In Legay A, Margaria T, editors, Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Vol. Part II. Berlin, Heidelberg: Springer. 2017. p. 151-168. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-54580-5_9

JANI: Quantitative Model and Tool Interaction

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this