Logo des Repositoriums

Auflistung nach Schlagwort "verification"

1 - 5 von 5
  • Konferenzbeitrag
    Enhancing DO-178C/DO-331 Based Process-Oriented Build Tool: Integration of System Composer and Automated PIL Simulation
    (SE 2024 - Companion, 2024) Panchal, Purav; Dmitriev, Konstantin; Myschik, Stephan
    The growing utilization of software in safety-critical systems can be attributed to advancing technology and substantial interest within aerospace and space industries. However, this increased reliance on software to enhance avionic system functionality raises crucial safety questions, emphasizing the need for compliance with standards like DO-178C/DO-331. To facilitate development, a process-oriented build tool was created in MATLAB/Simulink. This tool enhances development efficiency and ensures adherence to established processes, offering benefits like modular software management, systematic artifact handling with traceability, seamless integration with various verification tools, automated model and code verification, and a well-defined design environment. Recently, two new advancements have been made to the tool, integration of System Composer for developing software architecture and automated processor-in-the-loop (PIL) verification using Trace32. This paper presents these new developments along with examples.
  • Konferenzbeitrag
    Privacy by Design Architecture Composed of Identity Agents Decentralizing Control over Digital Identity
    (Open Identity Summit 2020, 2020) Toth, Kalman C.; Cavoukian, Ann; Anderson-Priddy, Alan
    Proposed is an identity architecture that satisfies the principles of privacy by design, decentralizes control over digital identity from providers to users, mitigates breach and impersonation risks, and reduces dependency on remote access passwords. The architecture is composed of interoperating identity agents that work on behalf of their owners and deploy digital identities that are virtualized to look and behave like identities found in one’s wallet and contacts list. Encapsulating authentication data, identity agents strongly bind owners to their digital identities and private keys enabling them to prove who they are, protect their private data, secure transactions, conduct identity proofing, and reliably delegate consent. Identity agents also off-load application services from identity-related and privacy-related tasks. A gestalt privacy by design process has been used to discover the architecture’s privacy requirements and design elements and systematically reason about how the design elements satisfy the privacy requirements. Identity-related functionality has been intentionally compartmentalized within identity agents to focus development on creating trustworthy software. A reference model for development derived from the described identity architecture is proposed.
  • Zeitschriftenartikel
    A sampling-based approach for handling delays in continuous and hybrid systems
    (it - Information Technology: Vol. 63, No. 4, 2021) Berani Abdelwahab, Erzana; Fränzle, Martin
    Delays in feedback dynamics of coupled dynamical systems arise regularly, especially in embedded control where the physical plant and the controller continuously interact through digital networks. Systems featuring delays are however notoriously difficult to analyze. Consequently, formal analysis often addresses simplified, delay-free substitute models, risking negligence of the adverse impact of delay on control performance. In this ongoing work, we demonstrate that for continuous systems such as delay differential equations, a major part of the delay-induced complexity can be reduced effectively when adding natural constraints to the model of the delayed feedback channel, namely that it transports a band-limited signal and implements a non-punctual, distributed delay. The reduction is based on a sampling approach which is applicable when the above conditions on the feedback are satisfied. We further discuss the possibilities of lifting this method to mixed discrete-continuous dynamics of delayed hybrid systems and the open issues thereof.
  • Workshopbeitrag
    SMT Solvers – A PromisingWay for Verifying User Interfaces?
    (Mensch und Computer 2022 - Workshopband, 2022) Bruchertseifer, Jens; Weyers, Benjamin
    Evaluating user interfaces of interactive applications in terms of correctness has always been a lengthy and error-prone task, as it would be executed by humans. This has led to this aspect of development being severely neglected, which poses a fundamental problem in terms of usability. In this work, we present a novel approach based on the creation of a formal representation from a given user interface, which is transformed into a reference net and finally converted into an SMT formula. As SMT formulae can be evaluated easily using highly efficient SMT solvers, this approach promises good efficiency in real-world scenarios.
  • 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.