The JANI Specification Contact us

of the jani-model format and the jani-interaction protocol

 

Model format Model libraries Tool support

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, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges and Andrea Turrini:
JANI: Quantitative Model and Tool Interaction. TACAS (2) 2017: 151-168 [DOI] [Bibtex]

The jani-model format

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.

• jani-model specification
• die.jani example model

Model libraries

Several collections of JANI models from various sources are available for testing, benchmarking, and modelling:

• The Quantitative Verification Benchmark Set comprises more than 75 quantitative models in the jani-model format that originate from many different input languages, can be scaled in size and difficulty through various parameters, and come annotated with reference results;
• all of the more than 50 (parametric) timed automata models in the IMITATOR benchmarks library (v2.0), categorised and complemented by sample results, are also available in the jani-model format; and finally
• the original JANI Model Library provides a small collection of models created or translated to demonstrate JANI.

Tool support

The following tools currently support the JANI specification:

• ePMC (formerly IscasMC)
  extensions: derived-operators
  input: PRISM language to jani-model
  output: jani-model to PRISM language
• FIG
  extensions: derived-operators
  input: IOSA to jani-model
  output: jani-model to IOSA
• The Modest Toolset
  extensions: arrays, datatypes, derived-operators, functions, named-expressions, nondet-selection
  input: Modest to jani-model
  output: jani-model to Modest
• Storm
  extensions: derived-operators, named-expressions
  input: GSPN (in GreatSPN Editor and PNML formats), pGCL and PRISM language to jani-model
  

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

(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.

• jani-interaction specification