karma - A Refinement Tool for Concurrent Systems Specified using Temporal Logic as Assertion Language

Synopsis:

     karma [file]

karma takes as input a file, file, given on the command line, if there exists a non-option argument. Input is read from stdin otherwise. The contents of the list depend on the options chosen.

The wide-spectrum specificationa and programming language used is inspired by [vdMM00] - it is a refinement calculus language with LTL as assertion language.

karma exits with 0 on success >0 otherwise

OPTIONS:

   -l --lex

lex input only

   -p --parse

parse input only

   -v --validity

treat input as an LTL formula and apss it to NuSMV for model checking

   -r --refine rulename

refine input using refinement rule rulename

   -? --help

Display some help information

EXAMPLES:

ENVIRONMENT:

karma expects NuSMV to be in the path somewhere. (See http://nusmv.irst.itc.it/.)

FILES:

BUGS:

This documentation doesn't reflect the way karma works right now. Currently, karma takes all input from the command line instead of stdin or file.

REFERENCES:

[vdMM00] Ron van der Meyden and Yoram Moses. On refinement and temporal annotations. In Mathai 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, pages 185--201. Springer-Verlag, 2000.