Logo des Repositoriums

Auflistung nach Schlagwort "formal methods"

1 - 3 von 3
  • Conference Program
    1st Workshop on Avionics Systems and Software Engineering (AVIOSE'19)
    (Software Engineering and Software Management 2019, 2019) Annighöfer, Björn; Schweiger, Andreas; Reich, Marina
    Companies are struggling with the complexity of digital avionics systems. Millions of man months are required for the development of digital airborne systems. Moreover, the complexity of functions, the number of vehicles, and systems continuously rises. There is a high demand for more efficient methods and tools of systems and software engineering. The AVIOSE workshop establishes a new forum for the exchange for the people working on simplifying, shortening, and maturing the creation of avionics systems.
  • Textdokument
    SmartOS: An OS Architecture for Sustainable Embedded Systems
    (Tagungsband des FG-BS Frühjahrstreffens 2022, 2022) Scheipel, Tobias; Batista Ribeiro, Leandro; Sagaster, Tim; Baunach, Marcel
    The number of embedded devices is growing, and so are the concerns about dependability and sustainability. However, the life-span of modern devices is commonly very short, due to their lack of long-term maintainability in both hardware and software. This yields an increased amount of e-waste, as the individual devices are commonly very cheap and can therefore easily be replaced in case of (partial) obsolescence. In this work, we show an operating system architecture which is designed to make embedded systems more sustainable and prepared for long-term use. To do so, we implement a general basic architecture alongside extended concepts and special features within the operating system. Our approach is based on hardware/software co-design and the opportunity to update software as well as hardware in a modular way at runtime. Therefore, logic reconfiguration of the host platform, dynamic software composition and integration, as well as formal methods for verification and portability are supported.
  • ConferencePaper
    Tool Support for Correctness-by-Construction
    (Software Engineering 2021, 2021) Runge, Tobias; Schaefer, Ina; Cleophas, Loek; Thüm, Thomas; Kourie, Derrick; Watson, Bruce W.
    This work was published in International Conference on Fundamental Approaches to Software Engineering 2019. We tackled a fundamental problem of missing tool support of the correctness-by-construction (CbC) methodology that was proposed by Dijsktra and Hall and revised to a light-weight and more amenable version by Kourie and Watson. Correctness-by-construction (CbC) is an incremental approach to create programs using a set of small, easily applicable refinement rules that guarantee the correctness of the program with regard to its pre- and postcondition specifications. Our goal was to implement a functional and user-friendly IDE, so that developers will adapt to the CbC approach and benefit from its advantages (e.g., defects can be easily tracked through the refinement structure of the program). The tool has a hybrid textual and graphical IDE that programmers can use to refine a specification to a correct implementation. The textual editor fits to programmers that want to stay in their familiar environment, while the graphical editor highlights the refinement structure of the program to give visual feedback if errors occur using KeY as verification backend. The tool was evaluated regarding feasibility and effort to develop correct programs. Here, slight benefits in comparison to a standard verification approach were discovered.