CISPA
Browse

Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS

Download (567.89 kB)
thesis
posted on 2023-11-29, 18:05 authored by Maximilian Schwenger
The control logic of complex systems is based on experience: Trained experts steer a machine directly until they help develop an automated controller. Recently, this process was further improved by successfully incorporating machine learning techniques, where the controller was learned from tremendous amounts of empirical data. The resulting controller excels most of the time, especially in situations similar to ones occurring in the training data. In a safety-critical context, however, this is not enough, so formal guarantees about the behavior of the controller become crucial. When a full static analysis and subsequent verification is infeasible due to the complexity of the system, runtime monitoring is still applicable. It acts as a connecting link between the efficiency of trained controllers and formally verifiable guarantees. A runtime monitor assesses the system health based on sensor readings by using a specification that contains information about desired system states and their expected evolution over time. When the monitor encounters a violation of the specification, it raises an alarm. For complex systems, characterizing the desired behavior requires an expressive language. Moreover, provably correct behavior requires formal semantics and an evaluation algorithm with static guarantees on resource consumption to prevent crashes during runtime. This thesis presents formal semantics for the specification language RTLola and shows that it satisfies the aforementioned criteria by introducing an evaluation algorithm with static time and space bounds. The approach is evaluated based on examples from health monitoring and aircraft controllers.

History

Preferred Citation

Maximilian Schwenger. Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS. Master's thesis, Saarland University. 2020.

Supervisor

Finkbeiner, Bernd

Primary Research Area

  • Reliable Security Guarantees

CISPA Affiliation

  • No

Legacy Posted Date

2020-09-14

Institution

Saarland University

Open Access Type

  • Unknown

Thesis Type

  • PhD Thesis

BibTeX

@mastersthesis{cispa_all_3200, title = "Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS", author = "Schwenger, Maximilian", school = "Saarland University", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC