1. 2

Abstract: “This paper presents the deductive formal verification of high-level properties of control systems with theorem proving, using the Why3 tool. Properties that can be verified with this approach include stability, feedback gain, and robustness, among others. For the systems, modeled in Simulink, we propose three main steps to achieve the verification: specifying the properties of interest over the signals within the model using Simulink blocks, an automatic translation of the model into Why3, and the automatic verification of the properties with theorem provers in Why3.

We present a methodology to specify the properties in the model and a library of relevant assertion blocks (logic expressions), currently in development. The functionality of the blocks in the Simulink models are automatically translated to Why3 as ‘theories’ and verification goals by our tool implemented in MATLAB. A library of theories in Why3 corresponding to each supported block has been developed to facilitate the process of translation. The goals are automatically verified in Why3 with relevant theorem provers. A simple first-order discrete system is used to exemplify the specification of the Simulink model, the translation process from Simulink to the Why3 formal logic language, and the verification of Lyapunov stability.”

  1.  

  2. 2

    Interesting paper, thanks for posting.

    I’ll try to take a more detailed look later, but would be interesting to see how their approach scales to something actually useful. The system they are using as an example is rather simple, and they mention having used a 150s time limit for the solver. I guess this is only for the marginal/instable cases with gain >= 1, for which the solver apparently timed out? Wonder how much time the solver needed for the proven cases.

    While searching, found a follow-up paper with an interesting comparison of different model checkers for similar stuff from 2015. Hopefully you weren’t planning to post this next. :)

    1. 2

      I didn’t have it! So, thanks. I actually wasn’t looking for Simulink/Stateflow stuff this year. I just stumble on it periodically because of how I word searches. I might spend more time looking for them next year due to importance in embedded. Are there any open tools that are comparable to those and high quality enough for professionals?

      EDIT: Also interesting is it’s two women. I tried to find out what their other work was to see what’s industrially applicable. Both had pages at Britol, here and here, with Araiza-Illan now at ARTC. It’s heavy on industrial application. Araiza-Illan also posted four hours of verification proceedings to YouTube. Interestingly, Eder worked at XMOS on power-aware design. As Bristol is Cadence’s lead university per that page, she’s probably also feeding ideas into their verification groups. If not, she at least started with real-experience per this interview which I’m still watching right now.

      So, you found not only a paper but two women doing interesting work with strong ties to industry and/or real-world experience. Extra interesting. Also, now on my list to potentially hire if I get into verification. :)

      1. 2

        Re: Open alternatives - This is a topic where I’ve wanted to look into lately. Probably a large portion of normal data analysis people might do in plain old Matlab would be easily replaceable with Python and the common analysis libraries for it.

        As for Simulink/Stateflow: I’ve been meaning to play around with OpenModelica, as I would really like to have an open alternative available if I don’t have access to Simulink in the future. The tool has been in development for a long time (still very active, with EU-funded research projects developing it further), has a consortium backing it with major players involved, and has been used as a basis for industrial tools. It’s the only thing I would seriously consider as a realistic open source alternative. There’s also JModelica, which is another Modelica-language based open source tool from a swedish company (apparently they base their commercial tools on the open core developed with couple of Unis).

        Simulink was always a nice tool for building models of dynamic systems, continuous or discrete, as the graphical notation makes sense for the sort of stuff in control engineering or signal processing, where you would anyway draw block diagrams or similar charts to try to clarify things. However, at least in my experience, building any sort of non-trivial software-like logic with the graphical blocks always resulted in a horrible mess. The Stateflow addition with hierarchical state machines has been a really nice addition to help with that aspect (before moving to software-in-the-loop with generated code or custom code through the C-interface). I think OpenModelica should have an equally good system/solver for the typical control/signal processing stuff (I read somewhere that the solver should be somehow even better/faster than the Simulink-solvers due to a different approach internally), I’m not sure how well supported the FSM-stuff is. At least there should also be a C-interface, so it should fill most of my use cases. For use with HW-in-the-loop-simulators, both systems support the FMI/FMU-standards, so ideally that should also be covered, but I’ve only worked with dSpace, which is rather heavily integrated with Matlab/Simulink.

        I don’t know how the usability of the graphical editor with OpenModelica is. You could always just write Modelica directly, but somehow I was always put off by the syntax of the language. :)

        1. 2

          I submitted OpenModelica here before. I don’t know much about it past the description sounded really cool and general-purpose. Yeah, expanding it to have parity with or better methods than Simulink/Stateflow makes sense. I didn’t know about FMI/FMU. Looking at this article, it says FMI is Modelica project. It has a nice pro’s/con’s section comparing to Simulink where improvements might be made.

          I’m not sure about FMU’s. It looks like they’re like modules or executables produced as a result of doing FMI. Like class or jar files in Java maybe. Or am I pretty far off?

          re syntax. Add it to list of Better Language extracts to and integrates with Supported Language. :)

          1. 2

            I also have pretty much no experience actually using the FMI-standard, as I’ve been stuck with Simulink (and the S-functions also mentioned in that Wikipedia-article). My undertanding is, that the FMI-standard specifies a way to describe the interfaces (IO-points) and the internal logic, and FMUs are then models/modules implemented according to this standard. Modelica is going for an object-oriented approach, so I think thinking of FMUs as classes is probably a good analogy.

            Typically, at least in the S-function world, and I think it’s the same here, one defines the time derivative of each continuous state within the model, which are fed back to the solver/simulator executing the model, and it handles the numerical integration and feeds to integrals back to the FMU (See p.69 here). For discrete stuff in the S-function world one defines a step-function, which is executed by the simulator every x seconds to solve the next outputs, FMI-standard seems to have an event-based approach, but “time-based events” probably boils down to the same thing.

            I tried to dig up some meaningful examples outside the actual spec, but they were a bit hard to find.

            This paper has an example of an FMU-description in Modelica: http://www.ep.liu.se/ecp/056/003/ecp1105603.pdf (I assume then this could be used to generate the XML/C-interface described in the FMI-standard?)

            There are some tutorial slides here.

            1. 1

              It looks pretty complicated haha. I’ll probably have to try OpenModelica or Simulink some time in the future on small, realistic examples to learn how they work. Especially the thinking process behind it. Probably different than what I’m used to. Thanks for the examples, though. The transmission example particularly shows me how they use these tools.