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.

JANI: Quantitative Model and Tool Interaction / Budde, Carlos E.; C., Dehnert; E. M., Hahn; Hartmanns, Arnd; S., Junges; A., Turrini. - ELETTRONICO. - 10206:(2017), pp. 151-168. (Intervento presentato al convegno TACAS 2017: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Sweden nel 2017) [10.1007/978-3-662-54580-5_9].

JANI: Quantitative Model and Tool Interaction

Carlos E. Budde;
2017-01-01

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.
2017
TACAS 2017: Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems
GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND
Springer Verlag
978-3-662-54579-9
978-3-662-54580-5
Budde, Carlos E.; C., Dehnert; E. M., Hahn; Hartmanns, Arnd; S., Junges; A., Turrini
JANI: Quantitative Model and Tool Interaction / Budde, Carlos E.; C., Dehnert; E. M., Hahn; Hartmanns, Arnd; S., Junges; A., Turrini. - ELETTRONICO. - 10206:(2017), pp. 151-168. (Intervento presentato al convegno TACAS 2017: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Sweden nel 2017) [10.1007/978-3-662-54580-5_9].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/314687
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 52
  • ???jsp.display-item.citation.isi??? 46
social impact