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).

Show object

• Location: Deutsche Nationalbibliothek Frankfurt am Main
• Extent: Online-Ressource
• Language: Englisch
• Notes: Albert-Ludwigs-Universität Freiburg, Dissertation, 2016

Classification and Topics

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

Contributors, Places and Time

• Event: Veröffentlichung
• (where): Freiburg
• (who): Universität
• (when): 2016
• Creator: Dietsch, Daniel
• Contributor: Podelski, Andreas

Further information

• DOI: 10.6094/UNIFR/11159
• URN: urn:nbn:de:bsz:25-freidok-111593
• Rights: Der Zugriff auf das Objekt ist unbeschränkt möglich.