Spinroot

A forum for Spin users

You are not logged in.

#1 2011-01-11 17:04:38

ChrisH
Member
Registered: 2011-01-11
Posts: 1

Büchi Automata as input for verification

Hi,

I'm considering to use SPIN as an underlying model checker for an integrated verification procedure. During this procedure, I obtain a model that I would like to verify which is very close to a Büchi Automaton. Thus, it would be very easy to actually transform the model into a Büchi automaton. Now, I would like to verify a LTL formula on this Büchi Automaton.

Therefore, I have the question: Is it possible to load a Büchi automaton as a model for verification (in whatever format) into spin? In case it is possible, is there any documentation on this?

I only found out that I can enter never claim directly in terms of a Büchi automaton, but I did not find a similar function for the model to be verified.

Best regards,

Christian

Offline

#2 2011-01-12 04:38:40

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Büchi Automata as input for verification

[quote=ChrisH]Hi,

I'm considering to use SPIN as an underlying model checker for an integrated verification procedure. During this procedure, I obtain a model that I would like to verify which is very close to a Büchi Automaton. Thus, it would be very easy to actually transform the model into a Büchi automaton. Now, I would like to verify a LTL formula on this Büchi Automaton.

Therefore, I have the question: Is it possible to load a Büchi automaton as a model for verification (in whatever format) into spin? In case it is possible, is there any documentation on this?

I only found out that I can enter never claim directly in terms of a Büchi automaton, but I did not find a similar function for the model to be verified.

Best regards,

Christian[/quote]

Yes you can do this, provided you specify the automaton in Promela. This can be very simple, as a state transition system using goto's for the state transitions.
A never claim is only meant to specify a property. In Version 6 the preferred method is even not to use never claims explicitly, but to use inline ltl formulae instead (which then get translated by spin into never claims).

But just to be clear: any proctype in a Spin model can define Buchi accepting states -- you can find the accepting cycles by running the generated model checker pan with option -a (-a for locating accepting cycles). You do not need to add a separate never claim to be able to do this.

Offline

Board footer

Powered by FluxBB