Diese Seite auf deutsch
SearchProject leader: Prof. Dr. B. Möller
| Current projects: |
 |
|
| Start of project: 2002 |
- InopSys - Interoperability of Calculi for System Modelling, 2002
The use of different complementary views plays an important role in describing complex systems. There are a lot of models which are adequate for data, transitions, interaction, composition, and recursive definitions at any level to describe static and dynamic aspects. The goal of the project is the integration of different formal models into an interoperable toolkit.
Project description, Publications, Homepage
| Finished projects: |
|
|
| End of project: 2002 | 2000 | 1998 | 1995 | 1994 | 1993 | 1992 |
- Development of Graph Algorithms in Formal Calculi, 2002
The goal of the project was to find a manageable algebraic calculus that is particularly applicable to the derivation of generic and hence highly re-usable graph algorithms from their formal specifications. It turned out that, besides classical relational calculus, Kleene algebra with domain and codomain operators is very well suited for this.
Project description, Publications
- System Support for Algebraic System Calculation , 2002
The project served to establish a loose cooperation with Kestrel Institute at Palo Alto. It deals with the following themes: First, the Augsburg group will evaluate the Kestrel system SPECWARE for its suitability to support algebraic derivations. Second, Kestrel will investigate how the Augsburg formalization of structures on the heap can be applied in a concrete modelling and verification project.
Third, both groups will cooperate on the issue of formal, algebraic derivation of concurrent garbage collection algorithms.
Project description, Homepage, Publications - JPP - Impact of Multimedia to Support Teaching at the University, 2000
The bavarian government supports with this project the integration of multmedia in teaching at univerities. The output of the project is a java toolkit (JPP) to support teachers in using multimedia.
Project description, Homepage, Publications - Design Methodology for Reactive Systems , 1998
A first project goal was to obtain techniques for the stepwise development of reactive systems. Concretely, it was to be investigated whether Statecharts are suitable for the necessary refinement and transformation steps or whether the language has to be adapted to allow such steps. Next, the project developed techniques for partitioning Statecharts to allow their distributed implementation.
Project description, Publications
- New Hardware Design Methods (ESPRIT Working Group 8533 NADA), 1998
The project performed research on new, mathematically sound methods for the description and design of hardware systems. The term "hardware systems" was interpreted very generally to include architectures and circuits and also the hardware/software interface. Another goal was a draft definition of a next generation hardware description language (NGHDL) with a high level of abstraction and a clean and formally defined semantics.
Description aspects included general questions of timing, parameterisation and modularisation. The design techniques included verification, deductive design in the small and structured design in the large. The goal of the research on modelling was to elicit requirements on design methodologies and description languages. The project studied architectures, circuits, and emerging new paradigms for hardware systems, as well as various standard technologies, and led to unified mathematical models of hardware. Appropriate mathematical methods came from computation theory, higher order algebra, proof theory and timed process algebra. The developed techniques were demonstrated in representative case studies.
Project description, Homepage, Publications - Deductive Design of Parallel Software and Hardware Systems , 1995
A major project goal was a uniform formal design methodology for parallel software and hardware systems. The main case study concerned a circuit for an asynchronous bounded queue buffer that served also as one of the IFIP WG 10.2 Verification Benchmarks. The formal analysis showed that the circuit given there was faulty; the error could have been avoided by systematic application of the technique of Deductive Design. Further Research concerned the use of communication streams in description and development of hardware.
Project description, Publications - Specification of Computer Science Systems in Higher-Order Logic, 1994
The method of algebraic specification consists in characterizing data structures by their typical operations and the equational laws that hold between them. While initially this approach was restricted to operations of first order, the central project partners, K. Meinke and B. Möller, had performed pioneering work to extend it to the case of higher-order operations. The project was concerned with the further development of the underlying mathematical theory and with case studies on the applications of this method. In particular, it performed investigations on the classification of the expressiveness and on computability of models of higher-order specifications.
Project description, Publications
- Transformational Design of Parallel Algorithms, 1994
The goal of the project was to carry over the technique of transformational program development to the case of parallel algorithms for different classes of architectures and to allow their derivation from the problem-oriented specification of their input/output behaviour.
Project description, Publications - Formal Derivation of Digital Circuits, 1993
The project goal was to derive from the general rules of program construction more special ones that are particularly suited to the case of cirucit derivation.
Project description, Publications - Functional Modelling of Distributed Systems, 1992
The work aimed at a formal design frame, based on functional description techniques, in which distributed systems can be developed in a systematic fashion. Special attention was paid to circuit derivation.
Project description, Publications