Dr. Jürgen Bohn

 

1 Publications (with abstracts)

[BJ96]

Jürgen Bohn and Wil Janssen. A strategic approach to transformational design. In Industrial Benefit and Advances in Formal Methods (FME'96), volume 1051 of Lecture Notes in Computer Science, pages 609-628. Springer-Verlag, 1996.
[ bib | .ps.gz ]

[BH95]

Jürgen Bohn and Hardi Hungar. Traverdi - transformation and verification of distributed systems. Lecture Notes in Computer Science, 1009:317-???, 1995.
[ bib ]

[BR95a]

Jürgen Bohn and Stephan Rössig. On automatic and interactive design of communicating systems. ProCoS Document [OLD JB 2/2], University of Oldenburg, Department of Computer Science, Oldenburg, Germany, 1995.
[ bib | .ps.gz ]

[BR95c]

Jürgen Bohn and Stephan Rössig. Towards a design assistant for communicating systems. ProCoS Document [OLD JB 3/1], University of Oldenburg, Department of Computer Science, Oldenburg, Germany, 1995.
[ bib | .ps.gz ]

[BR95b]

Jürgen Bohn and Stephan Rössig. On automatic and interactive design of communicating systems. In E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95) (Aarhus, Denmark), volume 1019 of Lecture Notes in Computer Science, pages 216-237. Springer-Verlag, 1995.
[ bib ]

The design of provable correct software requires formal methods whose usage should be assisted by suitable tools. Following a transformational approach the design needs interactive user help when important design decisions have to be made. Nevertheless simple parts should be automated as far as possible. Ideally the user only guides the design process by indicating the design ideas which are then carried out automatically. Typically sequential implementations are more appropriate for automation while parallelization needs interaction to determine the intended program architecture. This paper presents a transformational approach to the design of distributed systems where environment and concurrently running components communicate via synchronous message passing along directed channels. System specifications that combine trace-based with state-based reasoning are gradually modified by application of transfromation rules until Occam-like programs are achieved finally. We consider interactive and automatic aspects of such a design process and illustrate our approach by sketching the development of a shared register implementation.

[BJ95]

J. Bohn and W. Janssen. From a single specification to many implementations - many roads lead to parallelism. Technical report, University of Oldenburg, Department of Computer Science, Oldenburg, Germany, 1995.
[ bib ]

[Boh94a]

Jürgen Bohn. Formal reasoning about specification and transformation of reactive systems, 1994. Draft version.
[ bib ]

[Boh94b]

Jürgen Bohn. Formal transformational reasoning about reactive systems in the theorem prover LAMBDA. In T. Melham and J. Camilleri, editors, Supplementary proceedings of the 7th international workshop on Higher Order Logic Theorem Proving and its Applications. University of Malta, 1994.
[ bib ]

[Boh94c]

Jürgen Bohn. Formalizing the SL/PL design approach in LAMBDA. ProCoS Document [OLD JB 1/1], University of Oldenburg, Department of Computer Science, Oldenburg, Germany, 1994.
[ bib | .ps.gz ]

[Boh93b]

Jürgen Bohn. Interaktive Synthese kommunizierender Systeme mit LAMBDA. In Th. Kropf, R. Kumar, and D. Schmid, editors, Formale Methoden zum Entwurf korrekter Systeme. GI/ITG-Workshop, University of Karlsruhe, Germany, 1993.
[ bib ]

[Boh93a]

Jürgen Bohn. Formalizing the transformational design of communicating systems in the theorem prover LAMBDA. In J. Heering, K. Meinke, and B. Möller, editors, Higher Order Algebra, Logic and Term Rewriting (HOA'93). CWI, Amsterdam, The Netherlands, 1993.
[ bib ]