The JANI specification defines the jani-model model interchange format and the jani-interaction tool interaction and automation protocol. Its goal is to reduce the effort required to develop verification tools and to foster tool interoperation and comparison. JANI data is encoded using the JSON data format, which makes it simple to parse and easy to extend. It is specified using the js-schema language and library.
JANI is focused on, but not limited to, quantitative verification of probabilistic models. Standard labelled transition systems or Kripke structures can be represented in jani-model, and the jani-interaction protocol can be used with any modelling formalism with a textual representation.
To refer to JANI in scientific publications, please cite the following paper:
Carlos E. Budde,
Ernst Moritz Hahn,
Sebastian Junges and
JANI: Quantitative Model and Tool Interaction. TACAS (2) 2017: 151-168 [DOI] [Bibtex]
The jani-model format defines a straightforward JSON representation of networks of various kinds of quantitative automata with variables. By providing discrete variables and a parallel composition operation, models with large or even infinite state spaces can be represented succinctly. jani-model includes a basic set of variable types, assignments and expressions with most common operations, and allows the specification of qualitative and quantitative properties for verification within a model.
Several collections of JANI models from various sources are available for testing, benchmarking, and modelling:
The following tools currently support the JANI specification:
To test the validity of jani-model files, e.g. when creating a tool that can generate jani-model files, we recommend using the converters mentioned above.
For example, the Modest Toolset's moconv tool can perform a jani-model to jani-model conversion that catches many (but not all) errors by running
modest moconv input.jani -O output.jani
(The jani-interaction protocol is currently without tool support and may be deprecated in the future unless there is community interest in reactivating it.)
The jani-interaction tool interaction and automation protocol is intended to provide a stable interface that allows the reuse of existing implementations from new tools, reduces setup problems by allowing communication between tools running on different machines, and allows for a common integrated graphical user interface for JANI-based verifiers. A jani-interaction session consists of the exchange of a number of JSON messages. This can occur in one of two ways: either remotely over the WebSocket network protocol, with each message transmitted in one WebSocket text message, or locally by the client starting the server tool and writing its messages into the server’s standard input stream, with the server writing its replies onto its standard output stream, one message per line.