Re: [isabelle] Model checking of Simulink components with Isabelle



Hi Igor,

I did not look at your definitions in detail nor do I know anything about
the problem domain but there a few general things I can say.

If you look closely at the proof state that you give to blast in the
theorem you want to prove at the end of the theory, you might see
that the definitions did not get unfolded as you wanted them to be. You can
remedy this by adding the attribute 'abs_def' to the definitional theorems
before unfolding them (e.g. 'CC_active_b7_def[abs_def]').

The second thing is that your are trying to prove an existential statement,
so the best way is to explicitly specify a witness.
(Use 'apply (rule exI[where x = <your witness>]')
I do not know what it looks like or if you need to construct it by
induction, etc.
Sometimes Isabelle proof methods can find such a witness automatically,
however given the complexity of the formulae involved,
I fear that you're out of luck here .

I hope that was somewhat helpful.

 Simon


On Sat, Oct 1, 2016 at 2:50 PM Shumeiko, Igor <igor.shumeiko at rwth-aachen.de>
wrote:

> Hallo,
>
>
>
>  I am trying to do model checking of Simulink components? with Isabelle
> and now a little bit stuck on the way.
>
>  In general we would like to compare two software components for
>  behavior equivalence. The components are represented by automaton made
>  from Simulink components.
>
> Since the theory file is a bit long, I attached it to the mail.
>
>  The problem of this task is that one component has 7 input ports (that
>  are programed in Isabelle as functions of time: V_V LU_s LD_s BF_pc PB_b
>  P_b CC_b  FTS_a_b) and the second one has 8 input ports. We are trying
>  to find a value the on the 8th port of the second component which make
>  both of components equal. (This value must exist.) After that the
>  plan is to prove it by induction on t (?).
>
>  The internal variable update functions
>  (pV_eF7, pV_eR7, pV_FF7, pV_eF8, pV_eR8, pV_FF8) are calculated from
>  port values taken on the previous time step (t-1). The functions pV_FF8
>  and pV_FF7 are recursive while the other are not. The output value
>  are CC_active_b7 and CC_active_b8 respectively.
>
>  If you have time, could you please take a look at the Isabelle code,
>  probably you can suggest the best way to prove such things or the
>  direction I have to go? Or you immediately see that my approach is
> totally wrong.
>
>
> Sorry for a not concrete question any help or advice is highly appreciated.
>
>
> Best regards,
>
> Igor
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.