Automatic Software Validation for Critical Infrastructures
Loading...
Authors
Author (Corporation)
Publication date
2022
Typ of student thesis
Master
Course of study
Collections
Type
11 - Student thesis
Editors
Editor (Corporation)
Supervisor
Parent work
Special issue
DOI of the original publication
Link
Series
Series number
Volume
Issue / Number
Pages / Duration
Patent number
Publisher / Publishing institution
Hochschule für Wirtschaft FHNW
Place of publication / Event location
Olten
Edition
Version
Programming language
Assignee
Practice partner / Client
Abstract
Critical Infrastructure Systems (CIS) need to be more reliable. CIS are present in most life aspects, including hospitals, factories, aviation, and governmental venues. With the surge of interest on the Internet of Things (IOT), the number of devices in use will likely continue increasing for years to come. However, since any of these systems contained essentially software or hardware, all of them can pose reliability risks as well. Finding software bugs in CIS depends on analyzing machine code, as the software is generally proprietary. Due to software complexity, manual testing is not enough to guarantee the correct behavior of software. One alternative to this limitation is known as Symbolic Execution (SE). SE is a formal verification method that simulates software execution using symbolic values instead of concrete ones. The execution starts with all input variables unconstrained, and assignments that use any input variable are encoded as logical expressions. Whenever a branch is reached, the SE engine checks which values the branch condition can assume. If more than one valid evaluation is possible, the execution forks, and a new process is created for each possibility. This thesis will apply the concept of SE on software systems and show its efficiency to find software bugs at the early stage of software development life cycle. Furthermore, it shows how this can be applied to improve certification process of software systems. This thesis uses the state-of-the-art SE tool KLEE [78] in order to assess the proposed technique.
Keywords
Subject (DDC)
Event
Exhibition start date
Exhibition end date
Conference start date
Conference end date
Date of the last check
ISBN
ISSN
Language
English
Created during FHNW affiliation
Yes
Strategic action fields FHNW
Publication status
Review
Open access category
License
Citation
Mahmoud, T. (2022). Automatic Software Validation for Critical Infrastructures [Hochschule für Wirtschaft FHNW]. https://irf.fhnw.ch/handle/11654/48660