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:
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.
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.
The following tools currently support the JANI specification: