|
REFINERHistory
The REFINER tool is a tool to be used in combination with explicit-state model checker toolsets such as CADP and mCRL2. It offers the functionality to reason about the correctness of the semantics of concurrent system designs. The semantics of the system must have been captured in a network of Labelled Transition Systems. REFINER has a number of functionalities: First of all, it can transform the semantics of a concurrent system design according to a user-defined transformation rule system. Not only can REFINER actually apply the transformation, it can also reason about property preservation of rule systems. The property must be formalised in a fragment of the mu-calculus, identified in Mateescu-Wijs-11. By analysing the rules in a rule system in relation to the synchronisation rules of the system network, REFINER can determine whether a given property is guaranteed to be preserved, without constructing the state space of the transformed system (transformation is actually not even done). Second of all, REFINER can compositionally verify the correctness of concurrent system designs, using a novel technique called Incremental Counter-Example Construction (ICC). In that case, it is assumed that the last LTS in the system order represents a (negation of a regular) safety property. REFINER can be operated both via the command-line, and via a graphical user interface. ICC is currently offered only via the command-line. The GUI offers the added possibility to create and edit transformation rule systems. The user can design rules, i.e. pairs of LTSs with (exclusive) glue-states, and non-glue-states. Exclusive glue-states are glue-states that can only be matched on process LTS states that have no other transitions than the ones appearing in the left pattern. Download links for both the tool and a set of example models for experimentation are provided on this page. REFINER is implemented in Python 3. It can be run from the command-line by launching the refiner script for command-line usage, and by launching the refiner-gui script for using the GUI version. TIP: Although not required, the command-line version of REFINER runs much faster when using the Pypy interpreter, instead of Python. When installed, the refiner script will detect it, and use it to run REFINER. REQUIRED PACKAGES: Python 3 or higher, the mCRL2 toolset RECOMMENDED PACKAGES: Pypy
|