Computer Science Colloquium: On Specifications for Verification of Automated Production Systems

Wednesday, December 20, 2017, 12:30pm

Location: Seminar room 2202, Main building of Computer Science Center, Ahornstr. 55

Speaker: Alexander Weigl, M.Sc., Karlsruhe Institute of Technology, Karlsruhe


In industrial practice today, correctness of automated production system (aPS) software is rarely verified using formal techniques, although they are mission-critical and have strict safety requirements. A reason for the lack of formal verification is the need to create functional specifications, which is a very labour-intensive task.

In the IMPROVE APS project we proposed two approaches to reduce specification effort:

* Regression Verification [ICFEM 2015, ISAM 2016]

We present a method for regression verification of PLC code, which allows one to prove that a new revision of the plant's software does not break existing intended behavior. Instead of a functional specification we use the old software revision as the specification.

* Generalized Test Tables [INDIN 2017, iFM 2017]

With Generalized Test Tables we propose a specification language for reactive systems, especially for automated production system, that is both comprehensible and sufficiently expressive. Generalized test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. The semantics of generalized test tables is based on a two-party game over infinite words.

The computer science lecturers invite interested people to join.