Correct System Design

Dr. Jürgen Bohn

On this page:

back to the mainpage.

 

go next top of page

1 Publications (BibTeX Source)




@INPROCEEDINGS{jbwj96,
  AUTHOR = { J{\"u}rgen Bohn and Wil Janssen },
  TITLE = { A Strategic Approach to Transformational Design },
  BOOKTITLE = {Industrial Benefit and Advances in Formal Methods (FME'96)},
  VOLUME = 1051,
  PAGES = {609--628},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1996,
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/jbwj96-fme.ps.gz}
}


@ARTICLE{jbhh95,
  AUTHOR = { J{\"u}rgen Bohn and Hardi Hungar },
  TITLE = { Traverdi -- Transformation and Verification of Distributed
Systems },
  JOURNAL = {Lecture Notes in Computer Science},
  PAGES = {317--???{}},
  EDITOR = { M. Broy and S. J\"anichen },
  PUBLISHER = {Springer-Verlag},
  VOLUME = 1009,
  YEAR = 1995
}


@TECHREPORT{jbsr95-procos-2,
  AUTHOR = { J{\"u}rgen Bohn and Stephan R{\"o}ssig },
  TITLE = { On Automatic and Interactive Design of Communicating
                  Systems },
  INSTITUTION = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
  TYPE = { ProCoS Document },
  NUMBER = {[OLD JB 2/2]},
  YEAR = 1995,
  URL = {http://csd.informatik.uni-oldenburg.de/pub/ProCoS/JB-2-2.ps.gz}
}


@TECHREPORT{jbsr95-procos-3,
  AUTHOR = { J{\"u}rgen Bohn and Stephan R{\"o}ssig },
  TITLE = { Towards a Design Assistant for Communicating Systems },
  INSTITUTION = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
  TYPE = { ProCoS Document },
  NUMBER = {[OLD JB 3/1]},
  YEAR = 1995,
  URL = {http://csd.informatik.uni-oldenburg.de/pub/ProCoS/JB-3-1.ps.gz}
}


@INPROCEEDINGS{jbsr95-tacas,
  AUTHOR = {J{\"u}rgen Bohn and Stephan R{\"o}ssig},
  TITLE = {On Automatic and Interactive Design of Communicating
Systems},
  EDITOR = {E. Brinksma and W. R. Cleaveland and K. G. Larsen and T.
    Margaria and B. Steffen},
  BOOKTITLE = {Proceedings of the 1st International Workshop on Tools and
    Algorithms for the Construction and Analysis of Systems (TACAS'95) (Aarhus,
Denmark)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1019,
  PAGES = {216--237},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1995,
  ABSTRACT = {
    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.\bibpar 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.
  }
}


@TECHREPORT{jbwj95,
  AUTHOR = {J. Bohn and W. Janssen},
  TITLE = {From a Single Specification to Many Implementations --
    Many roads lead to parallelism},
  INSTITUTION = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
  YEAR = 1995
}


@MISC{jb94,
  AUTHOR = { J{\"u}rgen Bohn },
  TITLE = { Formal Reasoning about Specification and Transformation
    of Reactive Systems },
  YEAR = 1994,
  NOTE = {Draft version}
}


@INPROCEEDINGS{jb94-hol,
  AUTHOR = { J{\"u}rgen Bohn },
  TITLE = { Formal Transformational Reasoning about Reactive Systems
    in the Theorem Prover {LAMBDA} },
  BOOKTITLE = { Supplementary proceedings of the 7th international
    workshop on Higher Order Logic Theorem Proving and its Applications },
  YEAR = 1994,
  EDITOR = { T. Melham and J. Camilleri },
  PUBLISHER = { University of Malta }
}


@TECHREPORT{jb94-procos,
  AUTHOR = { J{\"u}rgen Bohn },
  TITLE = { Formalizing the {SL/PL} design approach in {LAMBDA} },
  INSTITUTION = {University of Oldenburg, Department of Computer Science, Oldenburg, Germany},
  TYPE = { ProCoS Document },
  NUMBER = {[OLD JB 1/1]},
  YEAR = 1994,
  URL = {http://csd.informatik.uni-oldenburg.de/pub/ProCoS/JB-1-1.ps.gz}
}


@INPROCEEDINGS{jb93-gi,
  AUTHOR = { J{\"u}rgen Bohn },
  TITLE = { {I}nteraktive {S}ynthese kommunizierender {S}ysteme mit
{LAMBDA}},
  BOOKTITLE = { Formale Methoden zum Entwurf korrekter Systeme },
  YEAR = 1993,
  EDITOR = { Th. Kropf and R. Kumar and D. Schmid },
  ORGANIZATION = { GI/ITG--Workshop },
  PUBLISHER = { University of Karlsruhe, Germany }
}


@INPROCEEDINGS{jb93-hoa,
  AUTHOR = { J{\"u}rgen Bohn },
  TITLE = { Formalizing the Transformational Design of Communicating
    Systems in the Theorem Prover {LAMBDA} },
  BOOKTITLE = { Higher Order Algebra, Logic and Term Rewriting (HOA'93)},
  YEAR = 1993,
  EDITOR = {J. Heering and K. Meinke and B. M\"oller },
  PUBLISHER = { CWI, Amsterdam, The Netherlands }
}

 top of page go back