Data-driven safety specification with Contract Mining

Data-driven safety specification with Contract Mining

Handshake

Context

Cyber-physical systems are often used in safety-critical environments, for example cars, airplanes or medical devices. Ensuring (functional) safety is therefore a very important task in the development of the systems. Safety must also be ensured during operation, and updates must not violate safety guarantees. An important method to formally describe safety of systems are contracts. A contract specifies what guarantees a system provides when certain assumptions are met. Contract-based design (CBD) allows system developers and testers to check various features of the system design. These are mainly: composition of different contracts, consistency, compatibility, and refinement. 

Unfortunately, this methodology entails additional effort in development: additional specifications are required for each component, which have to be described manually. In addition, there is the challenge of how to deal with old, already fully developed systems that were not previously part of a safety-critical function. If these systems, which have already proven themselves in operation, are now to be used in a safety-critical function, they must also be re-specified with contracts. 

This Master's thesis is dedicated to the question: Can this be done any other way? Automated? Several publications have shown that it is possible to derive meaningful contracts based on data using neural networks, genetic algorithms, decision trees or clustering methods. The approach to be investigated in this thesis therefore aims to use collected data produced by the system in a simulation or during operation. For cyber-physical systems, Signal-temporal Logic (STL) is particularly suitable as a description language for contracts, which is why the focus is on mining STL specifications in particular.

Goals

  • Research on new methods and tools for mining STL specifications and other temporal logics 
  • Design and implementation of a suitable mining process 
  • Evaluation and comparison of the implemented method with methods from the literature using suitable test systems 

Requirements

  • Interest in data mining, machine learning, functional safety and formal methods 
  • Solid programming skills (Python/C++)
  • Reliable and independent way of working