Tool Integration in the UniForM-Workbench

  • C. Lüth
  • E. W. Karlsen
  • Kolyang
  • S. Westmeier
  • B. Wolff
Conference paper
Part of the Advances in Computing Science book series (ACS)


The need for tool support is widely acknowledged, in particular in the context of formal methods. Yet, there exist many different tools serving different formal methods, and no single formal method (let alone tool) covers all aspects of software development. In order to combine the advantages of various tools and methods, they are combined into one integrated Software Development Environment (SDE).


Formal Method File System Proof Obligation Tool Integration Version Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Bahlke, R. and Snelting, G. (1986). The PSG System: From Formal Language Definitions to Interactive Programming Environments. ACM Transactions on Programming Languages and Systems.Google Scholar
  2. Bloesch, A., Kazmierczak, E., Kearney, P., and Traynor, O. (1995). Cogito: A Methodology and System for Formal Development. International Journal of Software Engineering, 4 (3).Google Scholar
  3. ECMA (1994). Portable Common Tool Environment (PCTE)-Abstract Specification. European Computer Manufacturers Association, 3rd edition. Standard ECMA-149.Google Scholar
  4. Fröhlich, M. and Werner, M. (1997). daVinci V2.0.3 Online Documentation. Univer-sität Bremen,
  5. Habermann, A. and Notkin, D. (1985). Gandalf: Software Development Environments. IEEE Transactions on Software Engineering.Google Scholar
  6. Hudak, P., Peyton Jones, S. L., and Wadler, P. (1992). Report on the Programming Language Haskell–a non strict purely functional language, version 1.2. ACM SIGPLAN notices, 27 (5): 1–162.Google Scholar
  7. Karlsen, E. W. (1997a). Integrating Interactive Tools using Concurrent Haskell and Synchronous Events. In CLaPF’97: 2nd Latin-American Conference on Functional Programming.Google Scholar
  8. Karlsen, E. W. (1997b). The UniForM Concurrency Toolkit and its Extensions to Concurrent Haskell. In G WFP’97: Glasgow Workshop on Functional Programming.Google Scholar
  9. Karlsen, E. W. (1998a). Tool Integration in a Functional Setting. PhD thesis, Univer-sität Bremen. Forthcoming.Google Scholar
  10. Karlsen, E. W. (1998b). The UniForM-workbench — a higher order tool integration framework. In International Workshop on Current Trends in Applied Formal Methods,Boppard, Germany.Google Scholar
  11. Kolyang, Lüth, C., Meier, T., and Wolff, B. (1997). TAS and IsaWin: Generic interfaces for transformational program development and theorem proving. In Bidoit, M. and Dauchet, M., editors, TAPSOFT 97’: Theory and Practice of Software Development,number 1214 in LNCS, pages 855–859. Springer Verlag.Google Scholar
  12. Kolyang, Santen, T., and Wolff, B. (1996). A structure preserving encoding of Z in Isabelle/HOL. In von Wright, J., Grundy, J., and Harrison, J., editors, Theorem Proving in Higher Order Logics — 9th International Conference,number 1125 in Lecture Notes in Computer Science, pages 283–298. Springer Verlag.Google Scholar
  13. Krieg-Bruckner, B., Peleska, J., Olderog, E. R., Balzer, D., and Baer, A. (1996). Universal Formal Methods Workbench. In Grote, U. and Wolf, G., editors, Statusseminar des BMBF: Softwaretechnologie. Deutsche Forschungsanstalt für Luft-und Raumfahrt, Berlin. Available at
  14. Libes, D. (1991). expect: Scripts for Controlling Interactive Processes. In Computing Systems, Vol 4, No. 2.Google Scholar
  15. Luth, C., Karlsen, E. W., Kolyang, Westmeier, S., and Wolff, B. (1998). HOL-Z in the UniForM-workbench — a case study in tool integration for Z. In Bowen, J., editor, 11th International Conference of Z Users ZUM’98, number 1493 in Lecture Notes in Computer Science, pages 116–134, Berlin, Germany.Google Scholar
  16. Nagl, M., editor (1996). Building Tightly Integrated Software Development Environments: The IPSEN Approach,volume 1170 of Lecture Notes in Computer Science. Springer Verlag.Google Scholar
  17. Ousterhout, J. K. (1994). Tcl and the Tk Toolkit. Addison Wesley.Google Scholar
  18. Paulson, L. C. (1994). Isabelle - A Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer Verlag.Google Scholar
  19. Peyton Jones, S., Gordon, A., and Finne, S. (1996). Concurrent Haskell. In Principles of Programming Languages ‘86 (POPL’96), Florida.Google Scholar
  20. Reif, W., Schellhorn, G., and Stenzel, K. (1997). Proving system correctness withGoogle Scholar
  21. KIV. In Bidoit, M. and Dauchet, M., editors, TAPSOFT 97’: Theory and Practice of Software Development,number 1214 in LNCS, pages 859–862. Springer Verlag.Google Scholar
  22. Reps, T. (1983). Generating Language Based Environments. PhD Thesis, Cornell University. MIT Press.Google Scholar
  23. Roscoe, A. W. (1998). The Theory and Practice of Concurrency. Prentice Hall. Spivey, M. (1992). The Z Notation: A Reference Manual. Prentice Hall. 2nd edition.Google Scholar
  24. Tej, H. and Wolff, B. (1997). A corrected failure-divergence model for CSP in Isa-belle/HOL. In Fitzgerald, J., Jones, C. B., and Lucas, P., editors, Proceedings of the FME ‘87 — Industrial Applications and Strengthened Foundations of Formal Methods,number 1313 in LNCS, pages 318–337. Springer Verlag.Google Scholar
  25. Westmeier, S. (1998). Verwaltung versionierter persistenter Objekte in der UniForM WorkBench (UniForM OMS Toolkit).Master thesis, FB 3, Universität Bremen.Google Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • C. Lüth
  • E. W. Karlsen
  • Kolyang
  • S. Westmeier
  • B. Wolff

There are no affiliations available

Personalised recommendations