Sergey Bozhko is a PhD student at the Max Planck Institute for Software
Systems under the supervision of Björn Brandenburg. His research focuses
on real‐time systems, formal methods, and the application of probability
theory to real‐time systems. He has received multiple awards for his
research, including Best Paper award at RTSS and Outstanding Paper award
at ECRTS.

   Info

AG Audience

English

120 Minutes

Saarbrücken

The Prosa project demonstrated that mechanized human-readable real-time
systems (RTS) theory was a viable alternative to the mainstream
pen-and-paper approach. Unfortunately, this mechanization effort faced
two obstacles: (1) the mechanized proofs of real-time systems theory,
when designed naively, contain an excessive amount of duplication, and
(2) the stochastic approach to analyzing RTSs, which is growing in
popularity, seems beyond the reach of Prosa. The proposed thesis will
address these fundamental challenges in the mechanization of RTS theory.

With regard to the issue of extensible non-duplicate RTA proofs, this
work proposes the first abstract response-time analysis (RTA) of
uniprocessor RTSs mechanized in Coq. To illustrate the flexibility, we
propose instantiations of the abstract RTA to all combinations of three
different scheduling policies, four preemption policies, and four
processor-supply models as well as an instantiation of the abstract RTA
to account for the priority ceiling protocol (PCP) for fully-preemptive
fixed-priority scheduling and the four processor-supply models.

With regard to adapting the Prosa approach to stochastic RTS theory,
this work proposes the first mechanized specification of stochastic RTS
as well as the definition of probabilistic worst-case execution time
(pWCET) accompanied by mechanized proof of its adequacy. In short, the
proven adequacy theorem states that actual execution costs represented
via dependent random variables can be replaced with independent and
identically distributed (IID) random variables derived from pWCET. The
reduction from dependent random variables to IID random variables opens
the door to a wide variety of techniques from probability theory. To
demonstrate that the mechanization of stochastic RTA is feasible with
reasonable effort, we propose building on the adequacy theorem to
mechanize a state-of-the-art stochastic RTA, thus creating the first
mechanized stochastic RTA.

Gretchen Gravelle

+49 681 9303 9102

--email hidden

Yes

Kaiserslautern

G26

113

passcode not visible

logged in users only