© Universität Augsburg

KIV ist eine Werkzeug zur formalen Systementwicklung und interaktiven Verifkation. Es kann eingesetzt werden z.B.

  1. 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,
  2. zur semantischen Fundierung von Programmiersprachen von der Spezifikation der Semantik bis zu einem verifizierten Compiler,
  3. 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

Installation

KIV ist ein Eclipse Plugin, das von der unten angegebenen Update Seite installiert werden kann. Der Plugin hängt von Scala 2.12 ab, deshalb sollte die Scala-IDE, siehe http://scala-ide.org/download/sdk.html heruntergeladen werden.

 

Installationsschritte

  1. In der ScalaIDE Help → Install New Software ... wählen.
  2. Die Update Seite für KIV für Eclipse https://swt.informatik.uni-augsburg.de/kiv/v9/stable/site eintippen und die Features KIV Eclipse Integration und  KIV Standard Library mit allen notwendigen Abhänigkeiten wählen.
  3. Nach dem Neustart von Eclipse kann die KIV-Perspektive unter Window, dann Open Perspective → Other geöffnet werden.
  4. 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 (andere Versionen sind aktuell ungetestet)

 

Ältere Eclipse Update Seiten

 

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.

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.

Suche