Das KIV System
KIV ist eine Werkzeug zur formalen Systementwicklung und interaktiven Verifkation. Es kann eingesetzt werden z.B.
- für die Entwicklung von sicherheitskritischen Systemen (Safety) von der formalen Anforderungsspezifikation bis hin zu ausführbarem Code, einschlie?lich der Verifikation von Sicherheit und Korrektheit der Implementierung,
- zur semantischen Fundierung von Programmiersprachen von der Spezifikation der Semantik bis zu einem verifizierten Compiler,
- für die Definition von Security-Modellen und Architekturmodellen wie sie für die Zertifizierung nach ITSEC oder CC ben?tigt werden.
Besondere Sorgfalt legt KIV darauf, starke Beweisunterstützung für alle Verifikationsaufgaben zu bieten. KIV unterstützt gro?e formale Modelle mit effizienten Beweistechniken und einer ergonomischen graphischen Benutzeroberfl?che. KIV wurde in einer Reihe von industriellen Pilotanwendungen und Forschungsprojekten eingesetzt, ist aber auch nützlich als Werkzeug in Kursen zu formalen Methoden in der Lehre.
?
KIV ist in der Programmiersprache Scala programmiert und als Plugin in die Eclipse-Plattform integriert.
News
- September 2024 Neues Visual Studio Code Plugin: Download und Installation.
- April 2023 KIV v10: verschiedene Korrekturen und Verbesserungen. Das Dateiformat hat sich gegenüber v9 ge?ndert. Wenn Sie ein altes Projekt konvertieren müssen, wenden Sie sich bitte per E-Mail an Gerhard Schellhorn.
- Juli 2022 Neues ?berblickspapier zum KIV System: Software & System Verification with KIV.
- April 2022 Geupdatete Version des KIV Plugins, die mit aktuellen Versionen der Eclipse IDE kompatibel ist.
- Mai 2021 Teilnahme am VerifyThis Verifikationswettbewerb (Best Student Team), mit L?sungen.
- Mai 2019 Teilnahme am VerifyThis Verifikationswettbewerb, mit L?sungen.
- Oktober 2018 KIV v9: verschiedene Korrekturen und Verbesserungen. Das Dateiformat hat sich gegenüber v8 ge?ndert. Wenn Sie ein altes Projekt konvertieren müssen, wenden Sie sich bitte per E-Mail an Gerhard Schellhorn.
- November 2017 Teilnahme am VerifyThis Verifikationswettbewerb (Best Student Team), mit L?sungen.
Installation in Eclipse
KIV ist ein Eclipse IDE Plugin, das von der unten angegebenen Update Seite installiert werden kann.
?
Installationsschritte
- ?ber die Eclipse Downloadseite ( https://www.eclipse.org/downloads/packages/release/2022-03/r) die Eclipse IDE for Java Developers herunterladen und installieren. Es sollte dabei die Version 2022-03 (4.23) gew?hlt werden, bei neueren Eclipse Versionen kann es vereinzelt zu Problemen kommen. Sollte es mit der Version 2022-03 (4.23) ebenfalls Probleme geben, kann auch auf die Oxygen Variante zurückgegriffen werden ( https://www.eclipse.org/downloads/packages/release/oxygen/3a).
- In Eclipse ?Help“ → ?Install New Software...“ w?hlen.
- Die Update Seite für KIV für Eclipse https://kiv.isse.de/releases/v10/stable/site angeben und die Features KIV Eclipse Integration und? KIV Standard Library mit allen notwendigen Abh?nigkeiten w?hlen.
- Nach dem Neustart von Eclipse kann die KIV-Perspektive unter Window, dann Open Perspective?→ Other ge?ffnet werden.
- Die Kurzeinführung hilft beim Einstieg.
Für weitere Informationen kann auch die Eclipse Dokumentation "Updating and installing software" nützlich sein.
?
Voraussetzungen
- Java 1.8 oder neuer
- Eclipse Oxygen oder neuer (das Plugin wird in der auf Oxygen basierenden ScalaIDE entwickelt, weshalb andere Versionen aktuell weniger getestet sind)
?
Lizenzabkommen
Copyright (c) 2013-present Department of Software Engineering, Augsburg University KIV is copyrighted by University of Augsburg, Formal Methods group of the chair of Software Engineering (Prof. Reif). This license grants the signer a non-transferable and non-exclusive right to use KIV. This license is restricted to noncommercial use. KIV is provided on an "as is" basis, without warranty or liability of any kind. The Licensee agrees not to modify, or disassemble any of the software files KIV consists of. This license is free of charge.
?
Die KIV Installation beinhaltet mehrere Bibliotheken. W?hrend der Installation werden Sie gefragt die jeweiligen Lizenzen ebenfalls zu akzeptieren.
Installation in Visual Studio Code
KIV ist inzwischen auch als Visual Studio Code Extension verfügbar. Diese umfasst allerdings noch nicht alle Features.
?
Installationsschritte
- ?ber die Visual Studio Code Webseite ( https://code.visualstudio.com/) die aktuellste Version herunterladen und installieren.
- Unter https://kiv.isse.de/releases/v10/vscode/latest/?die aktuellste Version der KIV Extension "kiv-editor-x.y.z.vsix" und der KIV Library Extension "kiv-library-x.y.z.vsix" herunterladen.
- In Visual Studio Code über die Navigationsleiste auf die ?Extensions“-View wechseln.
- Unter?Views and More Actions...“ → ?Install from VSIX...“ w?hlen und das heruntergeladene Archiv der KIV Extension selektieren (die Installation kann einen Moment dauern).
- Den Vorgang für die KIV Library Extension wiederholen.
- Nach der Installation sollte in der Navigationsleiste eine neue "KIV"-View angezeigt werden.
- Zur Aktivierung des KIV Syntax-Highlightings muss noch ein KIV-Theme aktiviert werden. Dazu ?File“ → ?Preferences“ → ?Theme“ → ?Color Theme“ w?hlen und eines der KIV-Themes ("KIV Light" oder "KIV Dark") selektieren.
?
Voraussetzungen
- Java 21 (oder neuer)
- Visual Studio Code
?
Lizenzabkommen
Copyright (c) 2013-present Department of Software Engineering, Augsburg University KIV is copyrighted by University of Augsburg, Formal Methods group of the chair of Software Engineering (Prof. Reif). This license grants the signer a non-transferable and non-exclusive right to use KIV. This license is restricted to noncommercial use. KIV is provided on an "as is" basis, without warranty or liability of any kind. The Licensee agrees not to modify, or disassemble any of the software files KIV consists of. This license is free of charge.
Institut für Software & Systems Engineering
Das Institut für Software & Systems Engineering, geleitet von Prof. Dr. Wolfgang Reif, ist eine wissenschaftliche Einrichtung in der Fakult?t für Angewandte Informatik an der Universit?t Augsburg. Das Institut unterstützt sowohl Grundlagen- als auch angewandte Forschung in allen Bereichen der Software & Systems Engineering. In der Lehre erm?glicht es die weitere Entwicklung des relevanten Kursangebots von Fakult?t und Universit?t.