Dunuen: A User-Friendly Formal Verification Tool

Formal verification allows checking the design and the behaviour of a system. One of the main limitations to the adoption of formal verification techniques is the process of model creation using specification languages. For this reason a tool supporting this activity is necessary. Actually, there are several tools allowing analysts to verify models expressed into specification languages. These tools provide support for automatically checking whether a system satisfies a property. However, to use such tools it is important to deeply know a precise notation for defining a system, i.e., the Calculus of Communicating Systems. Since systems are often expressed as time-series, to overcome this problem, we provide an user-friendly tool able to automatically generate a system model starting from the CSV - Comma-Separated Values format (the most widespread format considered to release dataset). In this way we hide the details about the model construction form the analyst, which can only focus immediately on the properties to verify. We introduce Dunuen, a tool allowing the user to firstly perform a kind of pre-processing operation starting from a CSV file, as discretization or removing attributes; subsequently it automatically creates a formal model from the pre-processed CSV file and, by invoking the model checker we embedded in Dunuen, it finally verifies whether the generated model satisfies a property expressed in temporal logic through a graphic interface, proposing formal methods as an alternative to machine learning for classification tasks. (C) 2019 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/) Peer-review under responsibility of KES International.