karma

Introduction

karma is the prototype of a refinement tool. The supported refinement calculus is closely related to the one presented in [vdMM2000]. Later versions are planned to support more ambitious refinement calculi, such as the ones described in [EvdMM2000] and [EvdMM2001].

System Requirements and Installation

karma is written in Haskell and uses nedit as interface. (The latter is likely to change in the near future.) Moreover, it depends on NuSMV to decide LTL formulae.

We use linux as development platform but there's no obvious reason why karma should not compile (and even run) on other unix-based systems such as Mac OS X and *BSD.

To build karma, simply type make in the top-level directory. The current GUI is NEdit (version 5.4RC1). The binary for this version can be found at nedit.org To interface karma NEdit needs a couple of macros stored in autoload.mn and information how to link the macros to its menu which is stored in nedit.rc (currently these are all preferences and thus will clash with your own .rc file). Copy nedit.rc and autoload.mn to your NEdit default directory as set in, e.g., .bashrc as export NEDIT_HOME=~/.nedit.

Code documentation.

Download

References

[vdMM2000]

Ron van der Meyden and Yoram Moses. On Refinement and Temporal Annotations. In M. Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, FTRTFT 2000 Pune, India, September 20—22, Proceedings, volume 1926 of LNCS, pp. 185—201. Springer-Verlag, 2000.