The correctness of the software used in control systems has been always a high priority, as a failure can cause serious expenses, injuries or loss of reputation. Our aim is to use formal methods in order to reduce the number of software bugs, preferably in the early phases of the development. Also, we try to make these methods accessible for the PLC community.
We work on two main aspects of formal methods:
- PLC formal verification : checking PLC software using model checking
- PLC formal specification : specifying PLC programs formally