Automatic Software Validation for
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  in order to assess the proposed
Mahmoud, Taha, 2022
Art der Arbeit Master Thesis
Betreuende Dozierende Scherb, Christopher
Studiengang: Business Information Systems (Master)