ISSE

Search

Formal Methods


Abstract

FormalMethods The institute is actively working on new techniques for formal system development. Our research focuses on refinement as a method of modular, step-wise, top-down development of a system starting with an abstract formal specification. The methodology for sequential systems is based on Abstract State Machines. Concurrent system analysis relies on the compositional temporal program logic "RGITL". Our group develops and distributes the KIV system, an interactive theorem prover that supports these techniques. Two of our current research projects are: VeriCAS (correctness of lock-free algorithms) and Flashix (development of a verified file system for flash memory).

Contact

Dr. Gerhard Schellhorn
E-Mail: schellhorn@informatik.uni-augsburg.de
Tel.: +49 821 598 - 2124

Researchers

Running Projects

  • Flashix
    Verification of a File System for Flash Memory

  • VeriCAS
    Verification of Lock-Free Concurrent Algorithms

Software

  • KIV System
    A tool for formal systems development and interactive verification

Services

  • Proving the functional correctness of safety- and security-critical systems
  • Consulting/training in the use of formal methods for the certification of software that meets the highest safety and security standards (e.g., SIL, Common Criteria)

Description

The goal of formal methods in software engineering is to provide techniques for developing highly reliable as well as security critical software. Two steps are required to achieve this goal: An unambiguous specification of the system requirements and a mathematical proof (verification) that the implementation adheres to this specification.
Formal methods provide a wide variety of mathematically precise specification languages, such as higher order logic, algebraic specifications, abstract state machines, the Z notation, and temporal logic. These languages enable the unambiguous description of a system's expected behavior, thereby forming the basis of the later verification of the system's correctness. System correctness consists of different aspects ranging from functional correctness to reliability.
Mathematical proofs of system correctness can be constructed using several approaches, such as interactive theorem proving, static code analysis, model checking, and SMT solving.
An important concept to handle complexity is refinement, which allows a modular, step-wise, top-down development of a system starting with an abstract formal specification.
We are actively working on new techniques for formal system development. Our research focuses on refinement in combination with abstract state machines and temporal logic. Our group is developing the KIV system, an interactive theorem prover. We apply these techniques in practical applications. Two of our current research projects are: VeriCAS (correctness of lock-free algorithms) and Flashix (development of a verified file system for flash memory).
We are offering our students lectures, lab courses, and seminars on formal methods and their application in the software engineering process.

Links