Skip to main content
SpringerLink
Log in

UniForM Perspectives for Formal Methods

  • Conference paper
Book cover Applied Formal Methods — FM-Trends 98 (FM-Trends 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1641))

Included in the following conference series:

Abstract

Trends for Formal Methods are reviewed and illustrated by several industrial applications: logical foundations of combination, verification, transformation, testing, and tool support. The UniForM Workbench is the background for highlighting experiences made over the past 20 years.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

7 References

  • Amthor, P., Dick, S. (1997): Test eines Bordcomputers für ein dezentrales Zugsteuerungssystem unter Verwendung des Werkzeuges VVT-RT. 7. Kolloquium Software-Entwicklung Methoden, Werkzeuge, Erfahrungen: Mächtigkeit der Software und ihre Beherrschung, Technische Akademie Esslingen.

    Google Scholar 

  • Astesiano, E. and Cerioli, M. (1994): Multiparadigm Specification Languages: a First Attempt at Foundations, In: C.M.D.J. Andrews and J.F. Groote (eds.), Semantics of Specification Languages (SoSl’93), Workshops in Computing, pp. 168–185. Springer.

    Google Scholar 

  • Blank Purper, C, Westmeier, S. (1998): A Graphical Development Process Assistant for Formal Methods. In: Proc. VISUAL’98 (short papers), at ETAPS’98, Lisbon. http://www.tzi.de/~uniform/gdpa

    Google Scholar 

  • Buth, B., Kouvaras, M., Peleska, J., Shi, H. (1997): Deadlock Analysis for a Fault-Tolerant System. In Johnson, M. (ed.): Algebraic Methodology and Software Technology. AMAST’97. LNCS 1349. Springer, pp. 60–75.

    Chapter  Google Scholar 

  • Buth, B., Peleska, J., Shi, H. (1998): Combining Methods for the Livelock Analysis of a Fault-Tolerant System. (submitted to AMAST’98)

    Google Scholar 

  • Cerioli, M., Haxthausen, A., Krieg-Brückner, Mossakowski, T. (1997): Permissive Order-sorted Partial Logic in CASL. AMAST’97. LNCS 1349. Springer.

    Google Scholar 

  • CoFI: The Common Framework Initiative for Algebraic Specification. http://www.brics.dk/Projects/CoFI

  • Diaconescu, R. (1998): Extra Theory Morphisms for Institutions: logical semantics for multi-paradigm languages. J. Applied Categorical Structures (to appear).

    Google Scholar 

  • Dierks, H. (1997): PLC-Automata: A New Class of Implementable Real-Time Automata. Proc. ARTS’97. LNCS 1231, pp. 111–125. Springer.

    Google Scholar 

  • Fischer, C. (1997): CSP-OZ: A Combination of Object-Z and CSP. In: Proc. Formal Methods for Open Object-Based Distributed Systems (FMOODS’ 97).

    Google Scholar 

  • Fröhlich, M. (1997): Inkrementelles Graphlayout im Visualisierungssystem daVinci. Dissertation. Monographs of the Bremen Institute of Safe Systems 6, Aachen, Shaker.

    Google Scholar 

  • Fröhlich, M., Werner, M. (1994): The interactive Graph-Visualization System daVinci — A User Interface for Applications. Informatik Bericht Nr. 5/94, Universität Bremen. updated documentation: http://www.tzi.de/~daVinci

  • H-PCTE (1996): The H-PCTE Crew: H-PCTE vs. PCTE, Version 2.8, Universität Siegen.

    Google Scholar 

  • Haxthausen, A. E., Peleska, J. (1998): Formal Development and Verification of a Distributed Railway Control System. In Proc. 1st FMERail Workshop, Utrecht, The Netherlands, (to appear).

    Google Scholar 

  • Hoffmann, B., Krieg-Brückner, B. (eds.) (1993): PROgram Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System. LNCS 680. Springer. http://www.tzi.de/~prospectra

    MATH  Google Scholar 

  • Karlsen, E. W. (1997a): The UniForM Concurrency ToolKit and its Extensions to Concurrent Haskell. In: O’Donnald, J. (ed.): GFPW’97, Glasgow Workshop on Functional Programming’ 97, Ullapool.

    Google Scholar 

  • Karlsen, E. W. (1997b): Integrating Interactive Tools using Concurrent Haskell and Synchronous Events, In ClaPF’97, 2nd Latin-American Conference on Functional Programming, La Plata, Argentina.

    Google Scholar 

  • Karlsen, E. W. (1998a): The UniForM WorkBench-a Higher Order Tool Integration Framework. In: International Workshop on Current Trends in Applied Formal Methods. LNCS. Springer (this volume).

    Google Scholar 

  • Karlsen, E. W. (1998b): Tool Integration in a Functional Setting. Dissertation. Universität Bremen. 364pp. (to appear).

    Google Scholar 

  • Karlsen, E. W., Westmeier, S. (1997): Using Concurrent Haskell to Develop User Interfaces over an Active Repository. In IFL’97, Implementation of Functional Languages 97, St. Andrew, Scotland, September 10–12, 1997. LNCS 1467. Springer.

    Google Scholar 

  • Kolyang (1997): HOL-Z, An Integrated Formal Support Environment for Z in Isabelle/HOL. Dissertation. Monographs of the Bremen Institute of Safe Systems 5, Aachen, Shaker.

    Google Scholar 

  • Kolyang, Lüth, C, Meyer, T., Wolff, B. (1997): TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving. In Bidoit, M. and Dauchet, M. (eds.): Theory and Practice of Software Development’ 97. LNCS 1214. pp. 855–859. Springer.

    Chapter  Google Scholar 

  • Kolyang, Santen, T., Wolff, B. (1996a): A Structure Preserving Encoding of Z in Isabelle/HOL. In Proc. Int’l Conf. on Theorem Proving in Higher Order Logic (Turku). LNCS 1125. Springer. http://www.tzi.de/~kol/HOL-Z

    Google Scholar 

  • Kolyang, Santen, T., Wolff, B. (1996b): Correct and User-Friendly Implementations of Transformation Systems. In: Gaudel, M.-C., Woodcock, J. (eds.): FME’96: Industrial Benefit and Advances in Formal Methods. LNCS 1051, pp. 629–648. Springer.

    Google Scholar 

  • Krieg-Brückner, B. (1996): Seven Years of COMPASS. In: Haveraaen, M., Owe, O., Dahl, O.-J. (eds.): Recent Trends in Data Type Specification. Proc. 11th ADT/COMPASS Workshop (Oslo 1995). LNCS 1130, pp. 1–13. Springer. http://www.tzi.de/~compass

    Google Scholar 

  • Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Balzer, D., Baer, A. (1996): UniForM, Universal Formal Methods Workbench. in: Grote, U., Wolf, G. (eds.): Statusseminar des BMBF: Softwaretechnologie. Deutsche Forschungsanstalt für Luft-und Raumfahrt, Berlin 337–356. See also http://www.tzi.de/~uniform

    Google Scholar 

  • Lankenau, A., Meyer, O., Krieg-Brückner, B. (1998): Safety in Robotics: The Bremen Autonomous Wheelchair. In: Proc. AMC’98, 5th Int. Workshop on Advanced Motion Control, Coimbra, Portugal 1998. ISBN 0-7803-4484-7, pp. 524–529.

    Google Scholar 

  • Lüth, C. (1997): Transformational Program Development in the UniForM Workbench. Selected Papers from the 8th Nordic Workshop on Programming Theory, Oslo, Dec. 1996. Oslo University Technical Report 248.

    Google Scholar 

  • Lüth, C. and Wolff, B. (1998): Functional Design and Implementation of Graphical User Interfaces for Theorem Provers. (to appear in Journal of Functional Programming).

    Google Scholar 

  • Lüth, C, Karlsen, E. W., Kolyang, Westmeier, S., Wolff, B. (1998a): Tool Integration in the UniForM WorkBench. In Berghammer, B., Buth, B., Berghammer, R., Peleska, J. (eds.): Tools for System Development and Verification. Workshop, Bremen, July 1996. Monographs of the Bremen Institute of Safe Systems 1, Aachen, Shaker.

    Google Scholar 

  • Lüth, C, Karlsen, E. W., Kolyang, Westmeier, S., Wolff, B. (1998b): HOL-Z in the UniForM WorkBench-a Case Study in Tool Integration for Z. Proc. ZUM’98, 11th International Conference of Z Users, LNCS 1493, pp. 116–134. Springer.

    Google Scholar 

  • Lüth, C., Shi, H., Krieg-Brückner, B. (1999): Abstraction in Transformational Developments. (submitted for publication).

    Google Scholar 

  • Lüth, C, Westmeier, S., Wolff, B. (1996): sml_tk: Functional Programming for Graphical User Interfaces. Informatik Bericht Nr. 8/96, Universität Bremen. http://www.tzi.de/~cxl/sml_tk

  • Mossakowski, T. (1996): Representations, Hierarchies and Graphs of Institutions. Dissertation. Monographs of the Bremen Institute of Safe Systems 2, Aachen, Shaker.

    Google Scholar 

  • Mossakowski, T. (1998): Translating other specification languages to CASL. Recent Trends in Algebraic Development Techniques. WADT’98, Lisbon. LNCS. (to appear)

    Google Scholar 

  • Mossakowski, T., Kolyang, Krieg-Brückner, B. (1998a): Static Semantic Analysis and Theorem Proving for CASL. In Parisi-Pressice, F. (ed.): Recent Trends in Algebraic Development Techniques. WADT’97, LNCS 1376, pp. 333–348. Springer.

    Google Scholar 

  • Mossakowski, T., Tarlecki, A., Pawlowski, W. (1997): Combining and Representing Logical Systems, In. Moggi, E. and Rosolini, G. (eds.): Category Theory and Computer Science, 7th Int. Conf. LNCS 1290, pp. 177–196. Springer.

    Chapter  Google Scholar 

  • Mossakowski, T., Tarlecki, A., Pawlowski, W. (1998b): Combining and Representing Logical Systems Using Model-Theoretic Parchments. In Parisi-Pressice, F. (ed.): Recent Trends in Algebraic Development Techniques. WADT’97, LNCS 1376, pp. 349–364. Springer.

    Google Scholar 

  • Mosses, P. (1997): CoFI: The Common Framework Initiative for Algebraic Specification and Development. In Bidoit, M. and Dauchet, M. (eds.): Theory and Practice of Software Development’ 97. LNCS 1214, pp 115–137. Springer.

    Chapter  Google Scholar 

  • Paulson, L. (1995): Isabelle: A generic theorem prover. LNCS 828. Springer.

    Google Scholar 

  • PCTE (1994): European Computer Manufacturers Association: Portable Common Tool Environment (PCTE), Abstract Specification, 3rd edition, ECMA-149. Geneva.

    Google Scholar 

  • Peleska, J. (1996): Formal Methods and the Development of Dependable Systems. Bericht 1/96, Universität Bremen, Fachbereich Mathematik und Informatik, 72p. http://www.tzi.de/~jp/papers/depend.ps.gz

  • Peleska, J., Siegel, M. (1996): From Testing Theory to Test Driver Implementation. in: M.-C. Gaudel, J. Woodcock (eds.): FME’96: Industrial Benefit and Advances in Formal Methods. LNCS 1051. Springer, pp. 538–556.

    Google Scholar 

  • Peleska, J., Siegel, M. (1997): Test Automation of Safety-Critical Reactive Systems. South African Computer Jounal 19, pp. 53–77.

    Google Scholar 

  • Sernadas, A., Sernadas, C., Caleiro, C. (1998a): Fibring of logics as a categorial construction. Journal of Logic and Computation 8(10), pp. 1–31.

    Google Scholar 

  • Sernadas, A., Sernadas, C., Caleiro, C., Mossakowski, T. (1998b): Categorical Fibring of Logics with Terms and Binding Operators. In Frontiers of Combining Systems-FroCoS’98. Kluwer Academic Publishers. To appear in Applied Logic Series.

    Google Scholar 

  • Tapken, J. (1997): Interactive and Compilative Simulation of PLC-Automata. In: Hahn, W. and Lehmann, A. (eds.): Simulation in Industry, ESS’97. SCS, pp. 552–556.

    Google Scholar 

  • Tapken, J. (1998): MOBY/PLC — A Design Tool for Hierarchical Real-Time Automata. System Demo. In: Astesiano, E. (ed.): Proc. First Int’l Conf. on Fundamental Approaches to Software Engineering, FASE’98, at ETAPS’98, Lisbon. LNCS. pp326–330. Springer.

    Chapter  Google Scholar 

  • Tarlecki, A. (1996): Moving between logical systems. In M. Haveraaen and O. Owe and O.-J. Dahl (eds.): Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types. LNCS 1130, pp. 478–502. Springer.

    Google Scholar 

  • Tej, Haykal (1999): HOL-CSP: Mechanised Formal Development of Concurrent Processes. Dissertation. Monographs of the Bremen Institute of Safe Systems. (forthcoming)

    Google Scholar 

  • Tej, H. and Wolff, B. (1997): A Corrected Failure-Divergence Model for CSP in Isabelle / HOL. Formal Methods Europe, Proc. FME’97, Graz. LNCS 1313, pp. 318–337. Springer.

    Google Scholar 

  • Urban, G., Kolinowitz, H.-L, Peleska, J. (1998): A Survivable Avionics System for Space Applications. in Proc. FTCS-28, 28 th Annual Symposium on Fault-Tolerant Computing, Munich, Germany, 1998.

    Google Scholar 

  • V-Model (1997): Development Standard for IT Systems of the Federal Republic of Germany. General Directives 250: Process Lifecycle; 251: Methods Allocation.

    Google Scholar 

  • Zhou, C, Hoare, C.A.R., Ravn, A.P. (1992): A Calculus of Durations. Information Processing Letters 40(5) pp. 269–276.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bremen Institute of Safe Systems TZI, FB3, University of Bremen, P.O. Box 330440, D-28334, Bremen

    Bernd Krieg-Brückner

Authors
  1. Bernd Krieg-Brückner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. German Research Center for Artificial Intelligence (DFKI GmbH), Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter  & Werner Stephan  & 

  2. Centro per la ricerca scientifica e tecnologica, ITC-irst, via Sommarive, 18, I-38050, Povo (Trento), Italy

    Paolo Traverso

  3. Bundesamt für Sicherheit in der Informationstechnik (BSI), Godesberger Allee 183, D-53175, Bonn, Germany

    Markus Ullmann

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Krieg-Brückner, B. (1999). UniForM Perspectives for Formal Methods. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds) Applied Formal Methods — FM-Trends 98. FM-Trends 1998. Lecture Notes in Computer Science, vol 1641. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48257-1_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-48257-1_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66462-8

  • Online ISBN: 978-3-540-48257-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation