Email Gateway (Aug 22 2022 at 14:12): Email Gateway (Aug 22 2022 at 14:12):From: "Shumeiko, Igor" <igor.shumeiko@rwth-aachen.de>
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
RMTComponents.thy
Email Gateway (Aug 22 2022 at 14:12):From: Simon Wimmer <wimmersimon@gmail.com>
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
Email Gateway (Aug 22 2022 at 14:16):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
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
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
Last updated: Nov 21 2024 at 12:39 UTC