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



Dear Igor,

I do not have a direct answer to your question, but I would like to let
you know
about the tool that we developed which translates Simulink diagrams into
Isabelle theories.

Using this tool one can check properties of Simulink diagrams in Isabelle
and for example one could check if two diagrams are equivalent.

The diagrams are represented in Isabelle as predicate transformers, and not
as functions as you have them in your example. The advantage of predicate
transformers is that we can model components that may fail for some input
values (e.g., division by zero).

Our tool contains a python script that takes as input a Simulink slx
file and
generates an Isabelle theory with "simulink" definitions for the
Simulink model.

We handle discrete as well as continuous models.

You can download our tool from

http://rcrs.cs.aalto.fi/

and you can download the paper describing it from here:

http://rcrs.cs.aalto.fi/papers/spin2016.pdf

The tool webpage contains links to some other relevant references
about the formal framework.

If you want to know more about it, or if you have problems using it,
please feel free to contact us.

Best regards,

Viorel Preoteasa & Iulia Dragomir



On 09/30/2016 04:12 PM, Shumeiko, Igor 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.