Short Description:
The task is to design and implement a translation from a PLC language to an analyzer back-end (such as NuSVM).
Background
Programmable logic controllers (PLCs) are industrial digital
computer control systems used e.g., to automate production processes or
execute process control. In many cases, the applications involve real-time
requirements and are, in addition, safety-critical. To program those
controller systems, domain-specific languages have been developed and
standardized (in the international IEC 61131-3 standard). Since those
systems are often used for safety-critical functions, for instance for oil
& gas production and transport systems in this context of the master
thesis, the code needs to undergo rigorous scrutiny to ensure its
functioning.
Problem setting:
One approach to verify PLC programs is model checking, i.e., to
exhaustively and automatically check whether a model of the given program
or system meets a given specification and thus is free of defects.
Currently, the PLC code for examples used in DNV-GL is manually converted
into a model (which then can be model-checked). Obviously, that process is
laborious, and error-prone in itself.
In this project, the task is to develop a compiler to read in PLC code and
then compile it into a model that can be analyzed using model checking tools. The task
includes the following:
- understand and work out the intended meaning of the PLC input
language (i.e., its semantics) - develop a parser/compiler that translates PLC programs to the input
language of a model checker (NuSMV, Maude) - model check a case study provided by DNV-GL.
Requirements:
Recommended knowledge includes acquaintance with parsing and compiler construction (or program analysis in general). Recommended courses include INF5140 (Specification and verification of parallel systems), which covers model-checking, and potentially other courses of PMA (about the Maude analyzer platform and/or static analysis).
Context
The master thesis will be carried out in collaboration with DNV-GL, and will allow to gain experience with state-of-the-art technologies used in an internationally leading company in technology certification and classification. The contact group in the company has expertise in developing, analyzing, and certifying system, in particular here, for PLC-based systems in the gas and oil sector. Furthermore, preliminary studies using NuSMV have been carried out. The PMA group at UiO likewise has expertise in tool-based verification and semantical analysis of software (for instance using model checking).