Executive Summary

Storm is a probabilistic model-checking software tool which is used for analysing stochastic aspects of systems like e.g. reliability, dependability, stochastic planning and controller synthesis (in robotics). Its core engines were developed in the last 5 years in the MOVES research group at RWTH Aachen University, Germany. DGB, with the technical support of MOVES group, will extend Storm into a commercial grade product. In the first phase, we will build/add 1) the graphical user interface (GUI) for input modelling languages, and 2) ability to automatically select Storm’s engines using AI/ML. GUI will improve the usability of the tool significantly, is important for demonstration purposes, and is a key enabler to industrial usage. It will feature a drag and drop editor for the input modelling languages of Storm such as Markov automata, Petri nets and dynamic fault trees; automatically translates these graphical models to the intermediate JANI language; and supports graphical displaying of Storm’s verification results. Whereas, automatic selection of Storm’s computational engines for given input models will increase its efficiency. Moreover, DGB will engage Information Technology University (ITU) for HR capacity building in formal methods. This will help DGB expand its team of experts with the aim of 1) offering formal verification services to industrial organizations using Storm, and 2) providing technical support to organizations that have licenses of a professional version of Storm. For the latter purpose, our company will further develop the prototypical GUI into a full-fledged GUI enabling the usage of Storm by non-experts. The rich breadth of the application areas of Storm, ranging from (embedded) software quality, reliability analysis of energy networks and defence equipment, to bottleneck analysis in railway networks, and biological systems, together with the experience and competences of the MOVES group as well as DGB make us believe that our endeavour will be successful. We have contacts to many potential customers in industry both in Europe and the USA; and as substantiated by recent reports in the USA, the cost of poor software quality is extremely high. That means, there is a high need for companies that help to improve software and ICT system’s quality that have stochastic aspects. The concept of a company that has a model-checking tool as its core business is not new. Successful examples exist in e.g., the Netherlands and Denmark. To our knowledge, DGB would be a pioneer for probabilistic model checking in the world. Given the enormous success of Storm --- it dominates the academic world-wide competitions, organized by QComp in 2019 and 2020, and its functionality goes beyond competitive tools --- and its maturity, we firmly believe that our technology is ready for this next quantum leap.

  • To train resources in formal methods specifically in probabilistic model-checking.
  • To start formal methods HR capacity building in Information Technology University (ITU).
  • To build the graphical editors for different input modelling languages of Storm such as Markov automata, Petri nets and dynamic fault trees.
  • To build translators for converting graphs of Markov automata, Petri nets and dynamic fault trees into intermediate JANI language and vice versa.
  • To build translators for converting properties of systems into JANI language and vice versa.
  • To build parsers for validating the syntax of input modelling languages of Storm such as Markov automata, Petri nets and dynamic fault trees.
  • To build modules for interacting with Storm to verify, experiment and simulate properties.
  • To build modules for displaying results of verification/experimentation/simulation in graphical form including Pareto curves for multi-objective analysis.
  • To build ML based module for automatic selection of Storm engines along with parameter selection for given input models.
  • To build modules for system configuration.
  • To test our modules/components for different benchmarks provided by MOVES group and as well as used in QComp competition.