Abstract
The UniForM Workbench supports combination of Formal Methods (on a solid logical foundation), provides tools for the development of hybrid, real-time or reactive systems, transformation, verification, validation and testing. Moreover, it comprises a universal framework for the integration of methods and tools in a common development environment. Several industrial case studies are described.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Amthor, P., Dick, S.: Test eines Bordcomputers für ein dezentrales Zugsteuerung system unter Verwendung des Werkzeuges VVT-RT. 7. Kolloquium Software Entwicklung Methoden, Werkzeuge, Erfahrungen: Mächtigkeit der Software und ihre Beherrschung, Technische Akademie Esslingen (1997).
Astesiano, E., Cerioli, M.: 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, Springer (1994) 168–185.
Blank Purper, C., Westmeier, S.: A Graphical Development Process Assistant for Formal Methods. In: Proc. VISUAL’98 (short papers), at ETAPS’98, Lisbon (1998). http://www.tzi.de/~uniform/gdpa
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. Proc. 4th DIMACS Workshop: Verification and Control of Hybrid Systems. New Brunswick, New Jersey, 1995.
Buth, B., Kouvaras, M., Peleska, J., Shi, H.: Deadlock Analysis for a Fault-Tolerant System. In Johnson, M. (ed.): Algebraic Methodology and Software Technology, AMAST’97. LNCS 1349. Springer (1997) 60–75.
Buth, B., Peleska, J., Shi, H.: Combining Methods for the Lovelock Analysis of a Fault-Tolerant System. In Haeberer, A.M. (ed.): Algebraic Methodology and Software Technology, AMAST’98. LNCS 1548. Springer (1999) 124–139.
Cerioli, M., Haxthausen, A., Krieg-Brückner, B., Mossakowski, T.: Permissive Subsorted Partial Logic in CASL. In Johnson, M. (ed.): Algebraic Methodology and Software Technology, AMAST 97, LNCS 1349, Springer (1997) 91–107.
CoFI: The Common Framework Initiative for Algebraic Specification and Development. http://www.brics.dk/Projects/CoFI
Diaconescu, R.: Extra Theory Morphisms for Institutions: logical semantics for multi-paradigm languages. J. Applied Categorical Structures 6 (1998) 427–453.
Dierks, H.: PLC-Automata: A New Class of Implementable Real-Time Automata. Proc. ARTS’97, LNCS 1231, Springer (1997) 111–125.
Dierks, H., Tapken, J.: Tool-Supported Hierarchical Design of Distributed Real-Time Systems. Euromicro Workshop on Real Time Systems, IEEE (1998) 222–229.
Dawsa, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: R. Alur, T.A. Henzinger, E.D. Sontag (Eds.): Hybrids Systems III-Verfication and Control. LNCS 1066, Springer, (1996).
Formal Systems Ltd.: Failures Divergence Refinement. User Manual and Tutorial Version 2.0. Formal Systems (Europe) Ltd. (1996).
Fischer, C.: CSP-OZ: A Combination of Object-Z and CSP. In H. Bowmann, J. Derrick (eds.): Formal Methods for Open Object-Based Distributed Systems, FMOODS’ 97, volume 2, Chapmann & Hall (1997) 423–438.
Fischer, C., Smith, G.: Combining CSP and Object-Z: Finite or infinite trace Semantics? Proc. FORTE/PSTV 97, Chapmann & Hall(1997) 503–518.
Fröhlich, M.: Inkrementelles Graphlayout im Visualisierung system daVinci. Dissertation. 1997. Monographs of the Bremen Institute of Safe Systems 6, ISBN 3-8265-4069-7, Shaker, 1998.
Fröhlich, M., Werner, M.: The interactive Graph-Visualization System daVinci A User Interface for Applications. Informatik Bericht Nr. 5/94, Universität Bremen, 1994. updated doc.: http://www.tzi.de/~daVinci
Hallerstede, S.: Die semantische Fundierung von CSP-Z. Diplomarbeit, Universität Oldenburg, 1997.
The H-PCTE Crew: H-PCTE vs. PCTE, Version 2.8, Universität Siegen, 1996.
Haxthausen, A. E., Peleska, J.: Formal Development and Verification of a Distributed Railway Control System. In Proc. 1st FMERail Workshop, Utrecht (1998).
Hoffmann, B., Krieg-Brückner, B. (eds.): PROgram Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System. LNCS 680. Springer, 1993. http://www.tzi.de/~prospectra
Karlsen, E.W.: The UniForM Concurrency ToolKit and its Extensions to Concurrent Haskell. In: O’Donnald, J. (ed.): GFPW’97, Glasgow Workshop on Functional Programming’ 97, Ullapool.
Karlsen, E.W.: Integrating Interactive Tools using Concurrent Haskell and Synchronous Events. In ClaPF’97, 2nd Latin-American Conference on Functional Programming, La Plata, Argentina (1997).
Karlsen, E.W.: The UniForM Workbench-a Higher Order Tool Integration Framework. In: Int’l Workshop on Current Trends in Applied Formal Methods. LNCS. Springer (to appear).
Karlsen, E.W.: Tool Integration in a Functional Setting. Dissertation. Universität Bremen (1998) 364pp (to appear)
Karlsen, E.W., Westmeier, S.: Using Concurrent Haskell to Develop User Interfaces over an Active Repository. In IFL’97, Implementation of Functional Languages 97, St. Andrew, Scotland. LNCS 1467. Springer (1997).
Kolyang: HOL-Z, An Integrated Formal Support Environment for Z in Isabelle/HOL. Dissertation, 1997. Monographs of the Bremen Institute of Safe Systems 5, ISBN 3-8265-4068-9, Shaker, 1998.
Kolyang, Santen, T., Wolff, B.: A Structure Preserving Encoding of Z in Isabelle/HOL. In Proc. Int’l Conf. on Theorem Proving in Higher Order Logic. LNCS 1125. Springer (1996). http://www.tzi.de/~kol/HOL-Z
Kolyang, Santen, T., Wolff, B.: 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 (1996) 629–648.
Krieg-Brückner, B.: Seven Years of COMPASS. In: Haveraaen, M., Owe, O., Dahl, O.-J. (eds.): Recent Trends in Data Type Specification, LNCS 1130 (1996) 1–13.
Krieg-Brückner, B.: UniForM Perspectives for Formal Methods. In: Int'l Workshop on Current Trends in Applied Formal Methods. LNCS. Springer (to appear).
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: Software technologie. Deutsche Forschungsanstalt für Luftund Raumfahrt, Berlin 337–356. http://www.tzi.de/~uniform
Kolyang, Lüth, C., Meyer, T., Wolff, B.: TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving. In Bidoit, M., Dauchet, M. (eds.): Theory and Practice of Software Development’ 97. LNCS 1214. Springer (1997) 855–859.
Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Balzer, D., Baer, A: UniForM Workbench, Universelle Entwicklungsumgebung für Formale Methoden; Schluβbericht. 1998. Monographs of the Bremen Institute of Safe Systems 9. ISBN 3-8265-3656-8. Shaker, 1999.
Lankenau, A., Meyer, O., Krieg-Brückner, B.: 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.
Lüth, C.: 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, May 1997.
Lüth, C. and Wolff, B.: Functional Design and Implementation of Graphical User Interfaces for Theorem Provers. J. of Functional Programming (to appear).
Lüth, C., Karlsen, E. W., Kolyang, Westmeier, S., Wolff, B.: HOL-Z in the UniForM Workbench-a Case Study in Tool Integration for Z. In J. Bowen, A. Fett,, M. Hinchey (eds.): Proc. ZUM’98, 11th International Conference of Z Users, LNCS 1493, Springer (1998) 116–134.
Lüth, C., Tej, H., Kolyang, Krieg-Brückner, B.: TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving. In J.-P. Finance (ed.): Fundamental Approaches to Software Engineering (FASE’99, at ETAPS’99). LNCS 1577. Springer (1999) 239–243. http://www.tzi.de/~agbkb
Lüth, C., Westmeier, S., Wolff, B.: sml_tk: Functional Programming for Graphical User Interfaces. Informatik Bericht Nr. 8/96, Universität Bremen. http://www.tzi.de/~cxl/sml_tk
Meyer, O.: Automated Test of a Power and Thermal Controller of a Satellite. In: Test Automation for Reactive Systems-Theory and Practice. Dagstuhl Seminar 98361, Schloss Dagstuhl, (1998).
Mossakowski, T.: Using limits of parchments to systematically construct institutions of partial algebras. In M. Haveraaen, O. Owe, O.-J. Dahl, eds.: Recent Trends in Data Type Specification, LNCS 1130, Springer (1996) 379–393.
Mosses, P.: CoFI: The Common Framework Initiative for Algebraic Specification and Development. In Bidoit, M., Dauchet, M. (eds.): Theory and Practice of Software Development’ 97. LNCS 1214, Springer (1997) 115–137.
Mossakowski, T.: Translating OBJ3 to CASL: the Institution Level. In J. L. Fiadeiro (ed.): Recent Trends in Algebraic Development Techniques. 13th Int’l Workshop, WADT’98, Lisbon, Selected Papers. LNCS 1589 (1999) 198–214.
Mossakowski, T.: Representation, Hierarchies and Graphs of Institutions. Dissertation, Universität Bremen, 1996. Revised version. Monographs of the Bremen Institute of Safe Systems 2, ISBN 3-8265-3653-3, Shaker, 1999.
Mossakowski, T., Kolyang, Krieg-Bröckner, B.: Static Semantic Analysis and Theorem Proving for CASL. In Parisi-Pressice, F. (ed.): Recent Trends in Algebraic Development Techniques. WADT’97, LNCS 1376, Springer (1998) 333–348.
Mossakowski, T., Tarlecki, A., Pawlowski, W.: Combining and Representing Logical Systems, In Moggi, E. and Rosolini, G. (eds.): Category Theory and Computer Science, 7th Int. Conf. LNCS 1290, Springer (1997) 177–196.
Mossakowski, T., Tarlecki, A., Pawlowski, W.: Combining and Representing Logical Systems Using Model-Theoretic Parchments. In Parisi-Pressice, F. (ed.): Recent Trends in Algebraic Development Techniques. WADT’97, LNCS 1376, Springer (1998) 349–364.
Olderog, E.-R.: Formal Methods in Real-Time Systems. In Proc. 10 th EuroMicro Workshop on Real Time Systems. IEEE Computer Society (1998) 254–263.
Paulson, L. C.: Isabelle: A Generic Theorem Prover. LNCS 828, 1995.
European Computer Manufacturers Association: Portable Common Tool Environment (PCTE), Abstract Specification, 3rd ed., ECMA-149. Geneva, 1994.
Peleska, J.: Formal Methods and the Development of Dependable Systems. Bericht 1/96, Universität Bremen, Fachbereich Mathematik und Informatik (1996) 72p. http://www.tzi.de/~jp/papers/depend.ps.gz
Peleska, J.: Test Automation for Safety-Critical Systems: Industrial Application and Future Developments. In: M.-C. Gaudel, J. Woodcock (eds.): FME’96: Industrial Benefit and Advances in Formal Methods. LNCS 1051 (1996) 39–59.
He, J., Hoare, C.A.R., Fränzle, M., Müller-Olm, M., Olderog, E.-R., Schenke, M., Hansen, M.R., Ravn, A.P., Rischel, H.: Provably Correct Systems. In H. Langmaack, W.-P., de Roever, J., Vytopil (Eds.): Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863, Springer (1994).288–335.
Peleska, J., Siegel, M.: 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 (1996) 538–556.
Peleska, J., Siegel, M.: Test Automation of Safety-Critical Reactive Systems. South African Computer Journal 19 (1997) 53–77. http://www.tzi.de/ ~jp/papers/sacj97.ps.gz
Purper, C.: GDPA: A Process Web-Center. Proc. 2nd Workshop on Software Engineering over the Internet, with ICSE’99, Los Angeles, 1999. http://www.sern.cpsc.ucalgary.ca/~maurer/ICSE99WS/Program.htm
Purper, C.: An Environment to support flexibility in process standards. Proc. 1 st IEEE Conf. on Standardization and Innovation in Information Technology. Aachen, 1999 (to appear).
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, 1997.
Schlingloff, H., Meyer, O., Hülsing, Th.: Correctness Analysis of an Embedded Controller. In Data Systems in Aerospace, DASIA’ 99, Lissabon (May 1999).
Sernadas, A., Sernadas, C., Caleiro, C.: Fibring of logics as a categorial construction. Journal of Logic and Computation 8:10 (1998) 1–31.
Sernadas, A., Sernadas, C., Caleiro, C., Mossakowski, T.: Categorical Fibring of Logics with Terms and Binding Operators. In Gabbay, D., van Rijke, M. (eds.): Frontiers of Combining Systems. Research Studies Press (to appear).
Tapken, J.: Interactive and Compilative Simulation of PLC-Automata. In Hahn, W., Lehmann, A. (eds.): Simulation in Industry, ESS‘97. Society for Computer Simulation (1997) 552–556.
Tapken, J.: MOBY/PLC-A Design Tool for Hierarchical Real-Time Automata. In: Astesiano, E. (ed.): Fundamental Approaches to Software Engineering, FASE’98, at ETAPS’98, Lisbon. LNCS 1382, Springer (1998) 326–329.
Tapken, J., Dierks, H.: Moby/PLC-Graphical Development of PLC-Automata. In Ravn, A.P., Rischel, H. (eds.): FTRTFT’98, LNCS 1486, Springer (1998) 311–314.
Tarlecki, A: Moving between logical systems. In M. Haveraaen, O. Owe, O.-J. Dahl, eds.: Recent Trends in Data Type Specifications, LNCS 1130, 478–502. Springer, 1996.
Tej, H. (1999): HOL-CSP: Mechanized Formal Development of Concurrent Processes. Dissertation. (forthcoming)
Tej, H., Wolff, B.: A Corrected Failure-Divergence Model for CSP in Isabelle / HOL. Formal Methods Europe, FME’97. LNCS 1313, Springer (1997) 318–337.
Urban, G., Kolinowitz, H.-J., Peleska, J.: A Survivable Avionics System for Space Applications. in Proc. FTCS-28, 28th Annual Symposium on Fault-Tolerant Computing, Munich, Germany, 1998.
V-Model: Development Standard for IT Systems of the Federal Republic of Germany. General Directives: 250: Process Lifecycle; 251: Methods Allocation; 252: Functional Tool Requirements. (1997).
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A Calculus of Durations. Information Processing Letters 40(5) (1992) 269–276.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krieg-Brückner, B., Peleska, J., Olderog, ER., Baer, A. (1999). The UniForM workbench a universal development environment for formal methods. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_13
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive