Logo des Repositoriums

Auflistung nach Schlagwort "Model Checking"

1 - 5 von 5
  • Konferenzbeitrag
    Applicability of Model Checking for Verifying Spacecraft Operational Designs
    (Modellierung 2024, 2024) Chrszon, Philipp; Maurer, Paulina; Saleip, George; Müller, Sascha; Fischer, Philipp M. ; Gerndt, Andreas; Felderer, Michael
    This is a summary of the paper Applicability of Model Checking for Verifying Spacecraft Operational Designs which has been published at the 26th International Conference on Model Driven Engineering Languages and Systems (MODELS 23).
  • Konferenzbeitrag
    Cooperative Test-Case Generation with Verifiers
    (Software Engineering 2020, 2020) Beyer, Dirk; Jakobs, Marie-Christine
    Software testing is widely applied in software quality assurance. Often, test suites fulfilling a certain coverage measure must be constructed. Manually constructing them is laborious. However, numerous automatic test-generation approaches exist. Due to various strengths and weaknesses of individual approaches, hybrid approaches, which combine different approaches, construct test suites that achieve higher coverage values than test suites generated by individual approaches. We propose the hybrid test-generation approach CoVeriTest. CoVeriTest is flexible, cooperative, and based on verification technology. It iteratively executes a sequence of verifiers that may exchange analysis information between each other and output a test case whenever they reach a test goal. The verifiers, their individual time limits, and which analysis information is exchanged between them is configurable. We experimented with different CoVeriTest configurations. The best configuration participated in the 1st International Competition on Software Testing (Test-Comp’19) and won the third place. This proves the value of our CoVeriTest approach.
  • Konferenzbeitrag
    Providing Evidence for Correct and Timely Functioning of Software Safety Mechanisms
    (Software Engineering 2023 Workshops, 2023) Becker, Jan Steffen; Koopmann, Björn; Stierand, Ingo; Westhofen, Lukas
    In many application domains, the development of safety-critical systems must follow standards that define process steps and artifacts to establish a comprehensive safety argumentation. Commonly, this involves the identification of hazards and risks as well as the formulation of a safety concept to mitigate these risks. The concept is decomposed into safety requirements, which are finally implemented in hardware and software. All steps must be covered by analyses to ensure that the concept is effective and correctly implemented. This work focuses on timing aspects of the safety concept, i.e., on how it can be ensured that risk mitigation occurs in time. Based on an industrial use case, we show how consistent timing specifications can be derived, decomposed, and implemented in a complete and sound way. The approach extends previous work on contract-based design and investigates on explicating failure modes and fault detection in contract specifications. Finally, we show how model checking can support the verification of safety concepts and their implementation.
  • Workshopbeitrag
    Symbolic Model Checking in the Modular State Space using Binary Decision Diagrams
    (AWPN 2024 workshop proceedings, 2024) Zech, Lukas
  • Konferenzbeitrag
    Verification of Plastic Interactive Systems
    (i-com: Vol. 14, No. 3, 2015) Oliveira, Raquel; Dupuy-Chessa, Sophie; Calvary, Gaëlle
    Interactive systems have largely evolved over the past years. Nowadays, different users can interact with systems on different devices and in different environments. The user interfaces (UIs) are expected to cope with such variety. Plastic UIs have the capacity to adapt to changes in their context of use while preserving usability. Such capability enhances UIs, however, it adds complexity on them. We propose an approach to verifying interactive systems considering this adaptation capability of the UIs. The approach applies two formal techniques: model checking, to the verification of properties over the system model, and equivalence checking, to compare different versions of a UI, thereby identifying different levels of UI equivalence. We apply the approach to a case study in the nuclear power plant domain in which several UI are analyzed, properties are verified, and the level of equivalence between them is demonstrated.