JANI: Quantitative Model and Tool Interaction

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

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

33 Citations (Scopus)


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 languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication23rd 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
EditorsAxel Legay, Tiziana Margaria
Place of PublicationBerlin, Heidelberg
Number of pages18
VolumePart II
ISBN (Electronic)978-3-662-54576-8
ISBN (Print)978-3-662-54579-9
Publication statusPublished - 2017
Event23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 - Uppsala, Sweden
Duration: 22 Apr 201729 Apr 2017
Conference number: 23

Publication series

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


Conference23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017
Abbreviated titleTACAS


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


Dive into the research topics of 'JANI: Quantitative Model and Tool Interaction'. Together they form a unique fingerprint.

Cite this