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 bachelor thesis is dedicated to the question: Can this be done differently? Automated? First publications have shown that valid contracts can be derived based on data using 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

  • Overview and research on known methods and tools for mining STL specifications. 
  • Selection of suitable tools, if necessary implementation of a further procedure  
  • Evaluation and comparison of the selected methods using a test data set.

Requirements

  • Interest in functional safety, formal methods and genetic algorithms
  • Solid programming skills (Python/C++)
  • Reliable and independent way of working