K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Dear Samira,

K Tool has an interface that allows the use of the Maude LTL model checker.
You find an example in
.../dist/examples/cink/ltlmc
The definition is documented, so it should be easy to use it and to understand how the properties are defined.
The syntax and semantics of the atomic propositions are defined in the two modules at the end of the definition.
Following the K convention for builtins, the syntax temporal operators is []Ltl, <>Ltl (see, e.g., programs/form-dekker.cink).

Dorel

On 14.04.2013 4:08, samira kherfellah wrote:

Hi all,

I know that K framework is a tool to redefine languages (syntax and
semantics). But how about model_checking and k? how to set properties to be
verified in a language, using K?

Sincerly,
Samira.

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user

-- 
======================================
Dorel Lucanu, Ph.D.
Department of Computer Science, director
Faculty of Computer Science
Alexandru Ioan Cuza University
Berthelot 16, 700483 Iasi, Romania
URL: www.infoiasi.ro/~dlucanu
Tel.: +40 232 201551
Fax.: +40 232 201490
======================================