Search code examples
formal-verificationformal-methods

Which system can i verify by using CSP(Communication Sequencial Process)?

Now at the end of the semester, I need to use CSP to verify some systems. However, I have found some systems, but none of them are suitable. Is there any system that is easy to verify and has not been done by others?

Can you recommend it to me?

Solution

  • CSP is best for control-dominated systems and gets a bit unwieldy for data-dominated systems.

    Control-dominated: Think things like elevator controllers, bank machines, traffic lights etc where at lot of 'system events' are happening, with not a lot of data attached to them (perhaps only a few parameters).

    Data-dominated: Think things like signal processing, rendering, etc. Lots of data FLOWING through a number of operations the system performs.

    Everything I've mentioned in the control dominated list above are examples of systems people model while learning CSP. Another suggestion when learning some formal methods is simple card/dice games with unambiguous rules.

    When learning CSP, it's also good to model a system where you want to PROVE something like:

    • absence of deadlock/livelock
    • absence of an unsafe state. for instance, if you were to model a traffic light controller, you'd want to show that no state is possible where the lights in two directions can be 'green' at the same time.