search

nikos-kekatos / SpaceEx-tutorials

SpaceEx tutorials and features
https://nikos-kekatos.github.io/SpaceEx-tutorials/
1 stars 2 forks source link

Hybridization method #2

Open taliapandans opened 3 years ago

taliapandans commented 3 years ago

Dear Mr. Kekatos, I'm Talia and currently a student in Leibniz Universität Hannover. I couldn't find your email address and decided to contact you in github. Right now I'm doing my thesis with title "Comparison of Reachability Analysis Tools for Analog Circuit Verification". I have read your dissertation "Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Design Process" about hybridization method in SpaceEx. I'm curious about the syntax of sx format in page 86 and 87. My questions are if the auxiliary variable u1 dynamics set to any or const is and should variable u1 in PWA approximation Fig 5.7 bind to the one in ODE Fig 5.6? Thank you in advance!

Best Regards, Talia

mforets commented 3 years ago

I couldn't find your email address

you can try Nikolaos.Kekatos at univ-grenoble-alpes.fr

if the auxiliary variable u1 dynamics set to any or const

i think it is set to const, ie. as a constant that belongs to a given range (from page 84 of the thesis):

The error is added as an uncontrolled variable with the previously estimated bounds. There are two options for SpaceEx to parse it (either to add as a variable in the invariant or as a constant that belongs to a range).

u1 in PWA approximation Fig 5.7 bind to the one in ODE Fig 5.6

yes, i think that's the idea: the value of u1 is taken from the PWA approximation and then fed into the ODEs as an input.

taliapandans commented 3 years ago

Thank you for your reply! It has been a huge help!

mforets commented 3 years ago

No problem, and good luck with your thesis! This is such an exciting topic :)

BTW, you may want to check our tool JuliaReach. A simple example of a circuit with operational amplifier can be found here. (feel free to ask in our issue tracker if you have further questions).