Static code analysis and formal methods for PLC software
- Thread starter jubnzv
- Start date
My many years experience of different industries is - it generally depends on the industry and commercial limitations. Most customers just want a working system regardless of domain languages or any other specific limitation of the hardware. Any bugs were generally your problem.
Certain large organisations want every stage in Software Design documented; good example being the Nuclear Industry. They triple check every stage - factory test used to be long and drawn out. But then you just couldn’t go to site and commission systems.
Certain large organisations want every stage in Software Design documented; good example being the Nuclear Industry. They triple check every stage - factory test used to be long and drawn out. But then you just couldn’t go to site and commission systems.
oneye14,
Thank you for your answer. It sounds reasonable that the customer wants to have a working system with no additional cost and no time required for verification.
I also encountered this situation while I was working in the embedded area on software written in C. When the customer requires additional safety guaranties (like SIL certification), this adds requirements to our development process, including static analysis and verification routines in accordance with a safety standard such as IEC61580.
I understand that this is necessary for low-level languages like C, C++ or Ada. These languages potentially have an opportunity to make a bug with memory access or something like this.
But I've never heard of using the same analysis/verification routines for PLC software written in high-level "safe" domain specific languages. The source code written on these languages can also contains errors in the memory (for example, in direct variables access), or just contains silly mistakes, added due to inattention of the developer. What's strange is the standards that describe these languages, does not contains any information about the need for analysis/verification.
So, I developed a tool for static code analysis of IEC61131-3 programs, which supports PLCOpen standard guidelines and a very simple abstract interpretation engine based on z3. We use it in our work projects, and it's fine. But I wonder if my utility could be useful to anyone else outside of my company, what kind of functionallity they will need. Or should I just give it to my employer, because it seems that nobody else use the analysis of PLC.
Thank you for your answer. It sounds reasonable that the customer wants to have a working system with no additional cost and no time required for verification.
I also encountered this situation while I was working in the embedded area on software written in C. When the customer requires additional safety guaranties (like SIL certification), this adds requirements to our development process, including static analysis and verification routines in accordance with a safety standard such as IEC61580.
I understand that this is necessary for low-level languages like C, C++ or Ada. These languages potentially have an opportunity to make a bug with memory access or something like this.
But I've never heard of using the same analysis/verification routines for PLC software written in high-level "safe" domain specific languages. The source code written on these languages can also contains errors in the memory (for example, in direct variables access), or just contains silly mistakes, added due to inattention of the developer. What's strange is the standards that describe these languages, does not contains any information about the need for analysis/verification.
So, I developed a tool for static code analysis of IEC61131-3 programs, which supports PLCOpen standard guidelines and a very simple abstract interpretation engine based on z3. We use it in our work projects, and it's fine. But I wonder if my utility could be useful to anyone else outside of my company, what kind of functionallity they will need. Or should I just give it to my employer, because it seems that nobody else use the analysis of PLC.
