Technische Universität Braunschweig
  • Studium & Lehre
    • Vor dem Studium
      • Informationen für Studieninteressierte
      • Studiengänge von A-Z
      • Bewerbung
      • Fit4TU - Self-Assessment
      • Beratungsangebote für Studieninteressierte
      • Warum Braunschweig?
    • Im Studium
      • Erstsemester-Hub
      • Semestertermine
      • Lehrveranstaltungen
      • Informationen für Erstsemester
      • Studien-ABC
      • Studienorganisation
      • Beratungsnavi
      • Zusatzqualifikationen
      • Finanzierung und Kosten
      • Besondere Studienbedingungen
      • Hinweise zum Coronavirus
      • Gesundheit & Wohlbefinden
      • Campusleben
    • Nach dem Studium
      • Exmatrikulation und Vorlegalisation
      • Nach dem Abschluss
      • Alumni
    • Strategien und Qualitätsmanagement
      • Strategiepapiere für Studium und Lehre
      • Studienqualitätsmittel
      • Studiengangsentwicklung
      • Qualitätsmanagement
      • Rechtliche Grundlagen
    • Für Lehrende
      • Informationen für Lehrende
      • Lernmanagementsystem Stud.IP
      • Lehre und Medienbildung
    • Kontakt
      • Studienservice-Center
      • Sag's uns - in Studium und Lehre
      • Zentrale Studienberatung
      • Immatrikulationsamt
      • Abteilung 16 - Studium und Lehre
      • Career Service
      • Projekthaus
  • Forschung
    • Forschungsprofil
      • Forschungsschwerpunkte
      • Exzellenzcluster
      • Forschungsprojekte
      • Forschungszentren
      • Forschungsprofile der Professuren
    • Wissenschaftlicher Nachwuchs
      • Förderung des wissenschaftlichen Nachwuchs
      • Promotion
      • Postdocs
      • Nachwuchsgruppenleitung
      • Junior Professur und Tenure-Track
      • Habilitation
      • Service-Angebote für Wissenschaftler*innen
    • Forschungsdaten & Transparenz
      • Transparenz in der Forschung
      • Forschungsdaten
      • Open Access Strategie
      • Digitale Forschungsanzeige
    • Forschungsförderung
      • Netzwerk Forschungsförderung
      • Datenbanken und Stiftungen
    • Kontakt
      • Forschungsservice
      • Graduiertenakademie
  • International
    • Internationale Studierende
      • Warum Braunschweig?
      • International Student Support
      • Studium mit Abschluss
      • Austauschstudium
      • Geflüchtete
      • TU Braunschweig Summer School
    • Wege ins Ausland
      • Studium im Ausland
      • Praktikum im Ausland
      • Lehren und Forschen im Ausland
      • Arbeiten im Ausland
    • Internationale Wissenschaftler*innen
      • Internationale Postdocs und Professor*innen
      • Internationale Promovierende
      • Service für gastgebende Einrichtungen
    • Sprachen und interkulturelle Kompetenzvermittlung
      • Deutsch lernen
      • Fremdsprachen lernen
      • Interkulturelle Kompetenzvermittlung
    • Internationales Profil
      • Internationalisierung
      • Internationale Kooperation
    • International House
      • Wir über uns
      • Kontakt & Sprechstunden
      • Aktuelles und Termine
      • Newsletter, Podcast & Videos
      • Stellenausschreibungen
  • Die TU Braunschweig
    • Unser Profil
      • Ziele & Werte
      • Ordnungen und Leitlinien
      • Allianzen & Partner
      • Die Initiative Hochschulentwicklung 2030
      • Internationale Strategie
      • Fakten & Zahlen
      • Unsere Geschichte
    • Karriere
      • Arbeiten an der TU
      • Stellenmarkt
      • Berufsausbildung an der TU
    • Wirtschaft & Unternehmen
      • Unternehmensgründung
      • Freunde & Förderer
    • Öffentlichkeit
      • Veranstaltungskalender
      • Check-in für Schüler*innen
      • Hochschulinformationstag (HIT)
      • Kinder-Uni
      • Gasthörer*innen & Senior*innenstudium
      • Nutzung der Universitätsbibliothek
    • Presse & Kommunikation
      • Stabsstelle Presse und Kommunikation
      • Medienservice
      • Ansprechpartner*innen
      • Tipps für Wissenschaftler*innen
      • Themen und Stories
    • Kontakt
      • Allgemeiner Kontakt
      • Anreise
      • Für Hinweisgeber
  • Struktur
    • Leitung & Verwaltung
      • Das Präsidium
      • Stabsstellen
      • Verwaltung
      • Organe, Statusgruppen und Kommissionen
    • Fakultäten
      • Carl-Friedrich-Gauß-Fakultät
      • Fakultät für Lebenswissenschaften
      • Fakultät Architektur, Bauingenieurwesen und Umweltwissenschaften
      • Fakultät für Maschinenbau
      • Fakultät für Elektrotechnik, Informationstechnik, Physik
      • Fakultät für Geistes- und Erziehungswissenschaften
    • Institute
      • Institute von A-Z
    • Einrichtungen
      • Universitätsbibliothek
      • Gauß-IT-Zentrum
      • Zentrale Personalentwicklung
      • International House
      • Projekthaus
      • Transfer- und Kooperationshaus
      • Hochschulsportzentrum
      • Einrichtungen von A-Z
    • Studierendenschaft
      • Studierendenparlament
      • Fachschaften
      • Studentische Wahlen
    • Lehrer*innenbildung
      • Lehrer*innenfortbildung
      • Forschung
    • Chancengleichheit
      • Gleichstellung
      • Familie
      • Diversität
    • Kontakt
      • Personensuche
  • Suche
  • Schnellzugriff
    • Personensuche
    • Webmail
    • cloud.TU Braunschweig
    • Messenger
    • Mensa
    • TUconnect (Studierendenportal)
    • Lehrveranstaltungen
    • Im Notfall
    • Stud.IP
    • UB Katalog
    • Status GITZ-Dienste
    • Störungsmeldung GB3
    • IT Self-Service
    • Informationsportal (Beschäftigte)
    • Beratungsnavi
    • Linksammlung
    • DE
    • EN
    • Facebook
    • Twitter
    • Instagram
    • YouTube
    • LinkedIn
Menü
  • Technische Universität Braunschweig
  • Struktur
  • Fakultäten
  • Carl-Friedrich-Gauß-Fakultät
  • Institute
  • Institut für Softwaretechnik und Fahrzeuginformatik
  • Research
  • Correctness-by-Construction (CbC)
Logo Institut für Softwaretechnik und Fahrzeuginformatik der TU Braunschweig
  • Research
    • RED SPLAT (Reverse Engineering von Softwareproduktlinien für Maschinen und Anlagenbau)
    • Artifice
    • Correctness-by-Construction (CbC)
    • CrESt (Collaborative Embedded Systems)
    • Deltas
    • HyVar (Hybrid Variability)
    • Scaves
    • spp1593
    • Vampires

Correctness-by-Construction (CbC)

Correctness-by-Construction (CbC)

ISF Expertise

Name: Correctness-by-Construction (CbC)

Projektzeitraum: Dezember 2017 - offen

Correctness-by-Construction (CbC) is an approach to incrementally create correct programs. CbC starts with an abstract Hoare triple {P} S {Q} consisting of a precondition P, an abstract statement S, and a postcondition Q. Hoare triples represent total correctness assertions that valuate only to true if, beginning from the precondition, the postcondition is met after executing the eventually defined concrete program. With CbC, the Hoare triple is successively refined using a set of refinement rules to a concrete implementation, which satisfies the specification. The correctness is guaranteed because every refinement rule is proven sound and preserves the correctness of the program. CbC is implemted in the tool CorC. CorC is a graphical and textual IDE to construct algorithms following the Correctness-by-Construction approach. It supports CbC developers to refine a program by a sequence of refinement steps and to verify the correctness of these refinement steps using a theorem prover.

Information Flow Control-by-Construction

Besides of verifying the functional correctness, refinements rules can also be utilized to ensure security of programs. An information flow policy defines how information may flow in a program (e.g., a flow from public to secret data is allowed, but the other way is prohibited). The extension of CbC to ensure security is called Information Flow Control-by-Construction (IFbC). Programs are constructed incrementally using refinement rules to follow an information flow policy. In every refinement step, security and functional correctness of the program is guaranteed, such that insecure programs are prohibited by construction. The information flow policy can be specified in any bounded upper semi-lattice (i.e., security levels are arranged in a partially ordered set representing the allowed direction of information flow). IFbC is implemented in an extension of CorC.

Correctness-by-Construction for Software Product Lines

Software product lines provide systematic reuse of software and other artifacts paired with variability mechanisms in the code to implement whole product families rather than single software products. The commonalities and differences of the single variants are communicated as features, whose relationships are often modelled in feature models. Guaranteeing the correctness of a product line is especially challenging because of the amount of possible variants resulting from the number of feature configurations and the variable code structures. To create a correct product line using CbC, we therefore extended the original CbC approach with a new refinement rule for a variability mechanism in the statements of the Hoare triple and combined it with contract composition for variability in the pre- and postcondition. We call this extension variational Correctness-by-Construction. VarCorC uses FeatureIDE and variational CbC to support the development of correct-by-construction software product lines.

Github: https://github.com/TUBS-ISF/CorC

Involvierte Mitarbeiter: Tabea Bordis, Tobias Runge, Ina Schaefer

Publikationen:

  • T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Lattice-Based Information Flow Control-by-Construction for Security-by-Design. In FormaliSE, 2020.
  • T. Bordis, T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Variational Correctness-by-Construction. In 14th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'20), 2020.
  • T. Runge, T. Thüm, L. Cleophas, I. Schaefer, B. W. Watson: Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative UserStudy. In REFINE, 2019.
  • T. Runge, I. Schaefer, L. Cleophas, T. Thüm, D. G. Kourie, B. W. Watson: Tool Support for Correctness-by-Construction, Proc. of the International Conference on Fundamental Approaches to Software Engineering (FASE), Springer, 2019.
  • T. Runge, I. Schaefer, A. Knüppel, L. Cleophas, D. G. Kourie, B. W. Watson: Tool support for Confidentiality by Construction. In HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT'18), 2018.
  • I. Schaefer, T. Runge, A. Knüppel, L. Cleophas, D. G. Kourie, B. W. Watson: Towards Confidentiality-by-Construction. In International Symposium on Leveraging Applications of Formal Methods, Springer, 2018.
ISF Expertise
Bildnachweise dieser Seite

Für alle

Stellen der TU Braunschweig
Jobbörse des Career Service
Merchandising
Sponsoring- & Spendenleistungen
Drittmittelgeförderte Forschungsprojekte
Vertrauenspersonen für Hinweisgeber

Für Studierende

Semestertermine
Lehrveranstaltungen
Studiengänge von A-Z
Informationen für Erstsemester
TUCard

Interne Tools

Status GITZ-Dienste
Handbuch für TYPO3 (Intern)
Corporate Design-Toolbox (Intern)
Glossar (DE-EN)
Meine Daten ändern
Hochschulöffentliche Bekanntmachungen

Kontakt

Technische Universität Braunschweig
Universitätsplatz 2
38106 Braunschweig
Postfach: 38092 Braunschweig
Telefon: +49 (0) 531 391-0

Anreise

© Technische Universität Braunschweig
Impressum Datenschutz Barrierefreiheit

Zur anonymisierten Reichweitenmessung nutzt die TU Braunschweig die Software Matomo. Die Daten dienen dazu, das Webangebot zu optimieren.
Weitere Informationen finden Sie in unserer Datenschutzerklärung.