Automated verification of system requirements and software specifications

Hochschulschrift

Zusammenfassung: Many small to medium-sized enterprises that specialise in electrical or communications engineering are challenged by the increasing importance of software in their – often safety-critical – products. For this reason they have a strong interest in subcontracting competent partners for software development tasks. Yet, many of those enterprises refrain from subcontracting because they assessthe associated risks as too high. This thesis presents a set of methods and tools based on formal methods that are useful in reducing those associated risks. We are concerned with software-defined systems, i.e., systems whose behaviour is solely controlled by a program and the input the program receives from the environment. We especially focus on systems whose controlling programaccesses its hardware via memory-mapped I/O.We present a method for validating requirements between stakeholders with different levels of expertise. Based on validated requirements, we present the IRS -method that reduces the problem of deciding whether a software-defined system satisfies the requirements to the problem of whether the controlling program satisfies its specification. We show the feasibility of the IRS -method through an industrial case-study. The case-study uses a class of state-of-the-art tools for proving program correctness (deductive verifiers).

Angaben zum Objekt

• Standort: Deutsche Nationalbibliothek Frankfurt am Main
• Umfang: Online-Ressource
• Sprache: Englisch
• Anmerkungen: Albert-Ludwigs-Universität Freiburg, Dissertation, 2016

Klassifikation und Themen

• Klassifikation: Informatik
• Schlagwort: Software Engineering ; Formale Methode ; Model Checking ; Requirements engineering ; Statische Analyse ; Cyber-physisches System

Beteiligte, Orts- und Zeitangaben

• Ereignis: Veröffentlichung
• (wo): Freiburg
• (wer): Universität
• (wann): 2016
• Urheber: Dietsch, Daniel
• Beteiligte Personen und Organisationen: Podelski, Andreas

Weitere Informationen

• DOI: 10.6094/UNIFR/11159
• URN: urn:nbn:de:bsz:25-freidok-111593
• Rechteinformation: Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Letzte Aktualisierung: 25.03.2025, 13:42 MEZ