[isabelle] Model checking of Simulink components with Isabelle


 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,


Attachment: RMTComponents.thy
Description: RMTComponents.thy

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