Jun 14, 2016: Arnd Hartmanns: JANI: Quantitative Model and Tool Interaction

June 14, 2016JANI: Quantitative Model and Tool Interaction
Room: HB 2BArnd Hartmanns

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 talk, I will present the JANI model format and tool interaction protocol. The format is 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 quantitative model checking, a field that is at a decisive point in its growth where a push for coordination and standardisation is both necessary and maximally beneficial. The ultimate purpose of JANI is to simplify tool development, encourage research cooperation, and pave the way for a future competition in quantitative model checking.