KIT | KIT-Bibliothek | Impressum | Datenschutz

Companion Material for the PhD thesis "Formal Specification and Verification for Automated Production Systems"

Weigl, Alexander ORCID iD icon

Abstract (englisch):

This archive contains the evaluation for "Formal Specification and
Verification for Automated Production Systems". In particular, you
find evaluation environments for Chapter 7 (Evaluation (PART I -
Generalized Test Tables)), 10 (Relational Test Tables), 11 (Provably
Forgetting of Information), and 12 (Modular Regression Verification).

For more details, refer to the READMEs of the individual sub-folders.

Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Institut für Theoretische Informatik (ITI)
Publikationstyp Forschungsdaten
Publikationsdatum 11.11.2021
Erstellungsdatum 01.08.2017 - 07.11.2021
Identifikator DOI: 10.5445/IR/1000139656
KITopen-ID: 1000139656
Lizenz Creative Commons Namensnennung – Nicht kommerziell – Weitergabe unter gleichen Bedingungen 4.0 International
Schlagwörter Formal Specification, Formal Verification, Automated Production Systems, Manufacturing Systems, nuXmv, IC3, Eldarica, SeaHorn
 Formal Specification and Verification for Automated Production Systems

                            Alexander Weigl

                          COMPANTION MATERIAL

This bundle contains companion material for the PhD thesis "Formal
Specification and Verification for Automated Production Systems". In
particular you find following items:

  1. Files of the evaluation of the chapters:

    • Chapter 07: Evaluation (PART I - Generalized Test Tables)
    • Chapter 10: Relational Test Tables
    • Chapter 11: Provably Forgetting of Information
    • Chapter 12: Modular Regression Verification

    Runtime artefacts and log files are included.

    Further details are given in the files of the

  2. Software for the evaluation

    • verifaps-lib: the developed library for the verification of automated
      production systems (GPL v3)
    • eldarica: used for verification of C files (BSD 3-clause license)
    • ic3ia: used for the of VMT files (generated by nuXmv) (GPL v3)

    Not included and required for some experiments are

    • nuXmv (Version: 1.1.1, and 2.0.0),
      model checker, not included due to license restrictions.
    • SeaHorn,
      C program verifier, not included due to its large space size

      SeaHorn can be easly obtained by Docker or Podman:

      $ podman run -ti seahorn/seahorn-llvm10:nightly
Art der Forschungsdaten Dataset
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page