Das Ziel dieser Bachelorarbeit ist es, eine Anforderungsanalyse für eine solche Triage-Software durchzuführen, deren Ergebnis zur Formulierung von weiteren Richtlinien genutzt werden könnte.

Zu Beginn geht der Theorieteil dieser Arbeit auf die Grundlagen der Ethik, sowohl im Bereich Medizin, als auch der Informatik, ein. Im Medizinteil wird sich vorwiegend auf die Triage konzentriert. Der Informatikteil stellt zwei ausgewählte Ansätze der Softwareentwicklung (Ethik- und Werte-basiert) vor und zeigt am Beispiel von Codes of Conduct (CoCs) warum die dadurch entstandenen Richtlinien nicht ausreichend sind.

Als Antwort auf die Unzulänglichkeit bisheriger Richtlinien wird dann das EDAP-Shema vorgestellt, welches die Grundlage für die Anforderungsanalyse bildet. Diese Analyse beinhaltet das Abwägen von derzeitigen gesetzlichen Regelungen für Triage im deutschsprachigen Raum, ethische Fragen, denen man sich stellen muss, und ethische Vorgaben, die bei der Entwicklung einer Triage-Software in Erwägung gezogen werden sollten.

Der Kern der Anforderungsanalyse ist eine Fallstudie, in der die Stakeholder (Informatiker, Mediziner und Personen aus der allgemeinen Bevölkerung) Fragen zu ihren ethischen Ansichten, ihren Sorgen und ihren Werten beantworten, die auf die Entwicklung einer Ethik-basierten Triage-Software hinzielen. Die Studie soll sicherstellen, dass die Bedürfnisse der Stakeholder in der Anforderungsanalyse angemessen berücksichtigt werden. Die Ergebnisse der Studie dienen zur Verfeinerung der Anforderungsanalyse, bzw. der Aktualisierung des EDAP-Schemas.

In recent years, some partial answers have been obtained: among others, the scenario approach and interval markov decision processes have provided tools that partly allow to reconcile this oxymoron: one can indeed learn the system from data, in a monte-carlo fashion, and provide statistical guarantees on the quality of the abstraction. In this talk, I'll first survey these recent breakthroughs. Then I'll depart from that approach (by assuming that the monte-carlo sampling provides infinite accuracy), and will investigate another challenge inherent with data-driven abstractions: these techniques implicitly make an assumption of Markovianity, which may be violated on the true system. I will show how this assumption can ruin the approach if improperly handled, and will propose ways to mitigate and control the induced error, by leveraging concepts from ergodic theory, symbolic dynamics, and probability theory.

Biography:

Raphael Jungers is a Professor at UCLouvain, Belgium, currently on sabbatical leave at Oxford University. His main interests lie in the fields of Computer Science, Graph Theory, Optimization and Control. He received a Ph.D. in Mathematical Engineering from UCLouvain (2008), and a M.Sc. in Applied Mathematics, both from the Ecole Centrale Paris, (2004), and from UCLouvain (2005).

He has held various invited positions, at the Université Libre de Bruxelles (2008-2009), at the Laboratory for Information and Decision Systems of the Massachusetts Institute of Technology (2009-2010), at the University of L´Aquila (2011, 2013, 2016), and at the University of California Los Angeles (2016-2017).

He is a FNRS, BAEF, and Fulbright fellow. He has been an Editor at large for the IEEE CDC, Associate Editor for the IEEE CSS Conference Editorial Board, and the journals NAHS (2015-2016; Senior Editor 2023-), Systems and Control Letters (2016-2017), IEEE Transactions on Automatic Control (2015-2020), Automatica (2020-). He was the recipient of the IBM Belgium 2009 award and a finalist of the ERCIM Cor Baayen award 2011. He was the co-recipient of the SICON best paper award 2013-2014, the HSCC2020 best paper award, and an ERC 2019 laureate.

1. Analyze functions under a user defined condition (e.g., a user restricts the values of parameter x of function foo to the interval [0;100])
2. We identify each function call automatically and try to infer all parameters.

This can then be used used for a large number of interesting applications:
One very simple would be fault localization: Here the allowed mutations are those that remove program statements, and the fitness is determined by a) the bug has to still be present and b) the shorter the program the fitter.
Another application would be to generate structure-wise simple programs that are still hard to solve or to generate programs that are easy to solve by verifier/approach A, but hard to solve by verifier/approach B.

In the end the challenging part here (and why this probably has not been done really for software verification) is to keep time per roundtrip low enough to get enough iterations. For that the idea would be to start use bounded model checking/ limit the analysis time. Other tactics like speculative execution or using some static method to predict the fitness might also be worth exploring.
From a techical point of view the goal is to use BenchExec for executing the mutated programs each round (and such reduce the wall time for each round).
The language used for implementation will be Python3, which allows to use the pycparser as a frontend.