WKTool is a verification tool for weighted Kripke structures. It permits the specification of systems by the means of a CCS-like language. Properties are expressed using a weighted dialect of computation tree logic.
The verification engine relies on fixed point computation on dependency graphs (See: Xinxin Liu, Scott A. Smolka: Simple Linear-Time Algorithms for Minimal Fixed Points). Queries may also be encoded in symbolic dependency graphs, which can be more efficient for large bounds. Moreover, the engine supports both global and on-the-fly exploration of the state-space.
You can try WKTool here. Note that this is mainly a proof of concept project, hence some parts of the source code could be more maintainable.
WKTool has a large set of dependencies, most notably coffee-script needs to be
installed. If coffee-script is installed, you can unpacked the node_modules.tar.gz
and cake will automatically load all dependencies from node_modules folder.
You can also install latests version of the dependencies with
npm install stylus jade pegjs@0.7.0 coffee-script node-watch minimatch connect.
Observe, that until somebody fixes it, we have locked to pegjs version 0.7.0.
WKTool is released under GNU GPLv3 unless stated otherwise. For licenses of the included libraries see their respective websites listed in the Credits.
WKTool would not have been possible without libraries; currently we depend on the following.
- Bootstrap front-end framework.
- CodeMirror a syntax highlighting editor.
- arbor.js a graph layout library.
- jQuery.
- PEG.js Parser generator.
- Buckets.js Data structure library.
- Jonas Finnemann Jensen
- Lars Kærlund Østergaard