Logo des Repositoriums

Auflistung nach Autor:in "Glesner, Sabine"

1 - 7 von 7
  • Konferenzbeitrag
    Comprehensible Decisions in Complex Self-Adaptive Systems
    (Software Engineering und Software Management 2018, 2018) Klös, Verena; Göthel, Thomas; Glesner, Sabine
    To cope with uncertain and statically unforeseen environment behaviour of complex systems, self-adaptivity has gained wide acceptance. While adaptation decisions are required to be close to optimal decisions, they at the same time should be efficient, comprehensible, and reusable. To achieve this, we have developed an engineering and analysis approach for self-learning self-adaptive systems based on our notion of timed adaptation rules. Through continuous evaluation and learning, inaccurate rules can be improved and new rules can be learned at run-time to cope with changing environments and system goals. A separate verification phase enables us to provide offline and online guarantees of evolving adaptation logics based on human-comprehensible formal models. Our approach, which incorporates the precise retracing of previous adaptation decisions, enables the understanding of the contexts in which certain adaptation decisions have been made, and assessing whether they have gained their expected effect in time within the system. This comprehensibility of complex decisions in self-adaptive systems enables the precise understanding and reuse of adaptation logics and provides trust in autonomous decision making.
  • Konferenzbeitrag
    A formal correctness proof for code generation from SSA form in Isabelle/HOL
    (Informatik 2004, Informatik verbindet, Band 2, Beiträge der 34. Jahrestagung der Gesellschaft für Informatik e.V. (GI), 2004) Blech, Jan Olaf; Glesner, Sabine
    Optimizations in compilers are the most error-prone phases in the compilation process. Since correct compilers are a vital precondition for software correctness, it is necessary to prove their correctness. We develop a formal semantics for static single assignment (SSA) intermediate representations and prove formally within the Isabelle/HOL theorem prover that a relatively simple form of code generation preserves the semantics of the transformed programs in SSA form. This formal correctness proof does not only verify the correctness of a certain class of code generation algorithms but also gives us a sufficient, easily checkable correctness criterion characterizing correct compilation results obtained from implementations (compilers) of these algorithms.
  • Konferenzbeitrag
    Logische und softwaretechnische Herausforderungen bei der Verifikationoptimierender Compiler
    (Software Engineering 2005, 2005) Glesner, Sabine; Blech, Jan Olaf
    Korrektheit von Compilern ist notwendige Voraussetzung für die Korrektheit der damit übersetzten Software. Insbesondere optimierende Compiler sind oft fehlerhaft. In diesem Papier stellen wir nach einem Überblick über den Stand der Forschung unsere neuen Arbeiten zur Verifikation optimierender Compiler vor. Dabei diskutieren wir zum einen, welche logischen Probleme sich bei der formalen Verifikation von Übersetzungsalgorithmen in Compilern mittels Theorembeweisern ergeben und welche Lösungen wir dafür entwickelt haben. Zum anderen zeigen wir, wie man die Korrektheit auch realer optimierender Compiler mit beträchtlichem Implementierungsumfang sicherstellen kann. Damit tragen unsere Ergebnisse zur Korrektheit von Compilern, einem wichtigen Werkzeug in der Softwaretechnik, bei. Außerdem entwickeln wir auf diese Weise Methoden, die auch in anderen Anwendungsbereichen zur Verifikation von Software eingesetzt werden können.
  • Konferenzbeitrag
    Making MPI intelligent
    (Software Engineering 2012. Workshopband, 2012) Tetzlaff, Dirk; Glesner, Sabine
    Mapping parallel applications to multi-processor architectures requires information about the execution times of the concurrent processes to find an optimal allocation and must take into account the interprocessor communication at runtime, whose overheads have emerged as the major performance limitation. However, both information cannot be statically known in advance. In this paper we present a sophisticated approach for mapping parallel MPI applications to concurrent architectures using machine learning techniques. This automatically generates heuristics that provide the compiler with knowledge of the considered runtime behavior, hence yielding more precise heuristics than those generated by pure static analyses. The heuristics can be used to direct the runtime environment of MPI, which enables the reallocation of processes to other processors at runtime and, furthermore, results in a better initial allocation of MPI processes.
  • Konferenzbeitrag
    Methods of model quality in the automotive area
    (Software Engineering 2014, 2014) Reichertdt, Robert; Glesner, Sabine
  • Konferenzbeitrag
    Strategische Bedeutung des Software Engineering für die Medizin
    (Software Engineering 2007 – Fachtagung des GI-Fachbereichs Softwaretechnik, 2007) Glesner, Sabine; Jähnichen, Stefan; Paech, Barbara; Rumpe, Bernhard; Wetter, Thomas; Winter, Alfred
    Im Rahmen des Workshops 2006 der Software Engineering Professorinnen und Professoren im deutschsprachigen Raum in Bad Windsheim vom 25.-27.09.06 wurde ein Manifest Qualität in der Medizin durch Software Engineering erstellt, das im folgenden kurz skizziert und auf der Softwaretechnik Tagung 2007 zur Diskussion gestellt wird.
  • Konferenzbeitrag
    Towards Identifying Spurious Paths in Combined Simulink/Stateflow Models
    (Informatik 2016, 2016) Mikulcak, Marcus; Göthel, Thomas; Herber, Paula; Glesner, Sabine