Both computer programs and embedded systems become more and more complex with the progress of technological innovation. Cyber-physical systems, such as self-driving vehicles, communications satellites or medical robots, are not only expensive and difficult to produce, but they also have high requirements with respect to consistency, safety and efficiency.
Making sure cyber-physical systems meet those requirements is therefore of the utmost importance and must be done as early as during the design stage of the production. While analyzing the design of a cyber-physical system or testing a prototype are valid (albeit potentially costly) strategies for small systems, they are completely unfeasible for most real-case examples.
Thankfully, there exists another strategy: (statistical) model checking. With a model of the system, it is possible to simulate executions of the system and check if no execution violates a given property.
The goal of this presentation is to present multiple new ideas and frameworks to solve important problems of statistical model checking: the local extremum problem, the spatiality problem, and the optimal stopping problem.
12/09/2022