Formal Methods
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. We are currently working on the Flashix project, which aims at the development of a verified file system for flash memory.
- Phone: +49 821 598 2124
- Email: schellhorn@informatik.uni-augsburginformatik.uni-augsburg.de ()
- Room 3016 (Building N)
Hot Topics
Refinement
Modular, step-wise, top-down development of a system starting with an abstract formal specification
Temporal Logic
Concurrent system analysis relying on the compositional temporal program logic "RGITL"
Interactive Theorem Proving
Development and application of interactive theorem proving tools and techniques
?
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 over safety and security 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, ending with verified code.
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, such as in our research projects
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.
Tools & Projects
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)
Completed Projects
Go!Card
Formal Methods for Secure Java Smart Cards
FORMOSA
Integrating Formal Models and Safety Analysis
InopSys
Interoperability of Calculi for System Modelling
Protocure
Ensuring Quality in Healthcare
Team
Institute for Software & Systems Engineering
The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.