[Uni [FB [TZI] [BISS]


Universelle Entwicklungsumgebung für
Formale Methoden

8. Literatur und Veröffentlichungen

Dieses Kapitel gliedert sich in 3 Teile: Literatur anderer Autoren, Veröffentlichungen der Antragsteller und ihrer Arbeitsgruppen vor Beginn des Projekts sowie im Rahmen des Projekts UniForM Workbench.

8.1. Literatur

[ACD 90] R. Alur, C. Courcoubetis and D. Dill. Model-Checking for Real-Time Systems. In: 5th IEEE Logic in Computer Science, 1990.

[ACPG 91] M. Abadi, L. Cardelli, B. Pierce, G. Plotkin: Dynamic Typing in a Statically Typed Language,. in: ACM Transactions on Programming Languages and Systems, 13(2):237-20, April 1991.

[AD 92] R. Alur and D. Dill. The Theory of Timed Automata. In [BHRR 92].

[AL 92] M. Abadi and L. Lamport. An old-fashioned recipe for real time. In [BHRR 92], 1-27.

[Bac 90] R.J.R. Back. Refinement calculus, Part II: Parallel and Reactive Programs. In J.W. de Bakker, W.P. de Roever and G. Rozenberg (Eds.), Stepwise Refinement of Distributed Systems - Models, Formalisms, Correctness, LNCS 430 (Springer-Verlag, 1990) 67-93. [BB 90] J.C.M. Baeten, J.A. Bergstra. Real time process algebra. Formal Aspects of Computing 3(2), 1991, 142-188.

[Bas 88] David Basin. An environment for automated reasoning about partial functions. In 9th International Conference On Automated Deduction, pages 101-110, Argonne, Illinois, 1988. Springer-Verlag.

[Bas 94] David Basin. Logic frameworks for logic programs. In 4th International Workshop on Logic Program Synthesis and Transformation, (LOPSTR'94), Pisa, Italy, June 1994. Springer-Verlag. To Appear.

[BBH 93] Richard Barnett, David Basin, and Jane Hesketh. A recursion planning analysis of inductive completion. Annals of Artificial Intelligence and Mathematics, 24(3-4):363-381, 1993.

[BBL 91] David Basin, Geoffrey M. Brown, and Miriam E. Leeser. Formally verified synthesis of combinational CMOS circuits. Integration: The International Journal of VLSI Design, 11:235-250, 1991.

[BC 93] David Basin and Robert Constable. Metalogical frameworks. In Gérard Huet and Gordon Plotkin, editors, Logical Environments, pages 1-29. Cambridge University Press, 1993.

[BdV 89] David Basin and Peter DelVecchio. Verification of combinational logic in {N}uprl. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, Ithaca, New York, 1989. Springer-Verlag.

[BHRR 92] J.W. de Bakker, C. Huizing, W.P. de Roever and G. Rozenberg (Eds.). Real Time: Theory in Practice. LNCS 600 (Springer-Verlag, 1992).

[BJ 95] Broy, M., Jähnichen, S. (eds.): KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Final Report. Lecture Notes in Computer Science 1009 (1995).

[Bjø 89] D. Bjørner et al. A ProCoS project description - ESPRIT BRA 3104. EATCS Bulletin, 39:60-73, 1989.

[BKLOS 91] Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., Sannella, D.(eds.): Algebraic System Specification and Development - A Survey and Annotated Bibliography. LNCS 501 (1991) 98p.

[Br 91] Broy, M.: Towards a Formal Foundation of the Specification and Description Language SDL. Formal Aspects of Computing 3 (1991), pp.21.

[Bro 92] M. Broy. Functional specification of time sensitive communicating systems. In M. Broy, editor, Programming and Mathematical Method, NATO ASI Series: Computer and System Sciences Vol. 88, pages 325-367. Springer-Verlag, 1992.

[Caga 90] M. R. Cagan: The HPSoftBench Environment. An Architecture for a New Generation of Software Tools. Hewlett-Packard Journal, 41(3):36-47, June 1990.

[CH 88] Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, pages 95-120, 1988.

[CM 88] K.M. Chandy and J. Misra. Parallel Program Design - A Foundation. Addison-Wesley, 1988.

[CO 92] A. Cant, M.Ozols: A verification environment for ML programs. In P. Lee (ed.): Workshop on ML and its Applications, San Francisco. ACM SIGPLAN Notices (1992) 151-156.

[Con 86] Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

[CRSS 94] Cyrluk D., S. Rajan, N. Shankar, and M.K. Srivas. Effective theorem proving for hardware verification. In Second International Conference On Theorem Proving In Circuit Deisgn: Theory, Practice and Experience, Bad Herrenalb, September 1994.

[DeM 79] DeMarco, T. Structured Analysis and System Specification. Prentice-Hall, 1979.

[DR 93] J. Davies, G.M. Reed: Specification and Proof in Real-Time CSP. Oxford Programming Research Group Monograph 1991. Cambridge University Press, 1993.

[ECMA 93a] European Computer Manufacturers Association: Reference Model for Frameworks of Software Engineering Environments, ECMA TR/553, 3rd Edition, Geneva, June 1993.

[ECMA 93b] European Computer Manufacturers Association: Portable Common Tool Environment (PCTE) Abstract Specification, ECMA 149, 2nd Edition, Geneva, June 1993.

[FFFH 89] S. Finn, M. Fourman, M. Francis, and R. Harris. Formal system design - interactive synthesis based on computer-assisted formal reasoning. Technical report, Abstract Hardware Ltd., 1989.

[GB 84] J.A. Goguen, R.M. Burstall. Introducing Institutions. LNCS 164. 1984, pp. 221 - 256.

[GB 92] J.A. Goguen, R.M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. J. ACM, vol. 39, N0. 1, pp 95 -146 (Jan. 1992).

[GMW 79] Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh {LCF}: A Mechanized Logic of Computation, LNCS 78, 1979.

[Gor 88] Michael J. Gordon. HOL: a proof generating system for higher-order logic. In Birtwistle and Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publisher, 1988.

[GS 90] W. Grieskamp, W. Schulte: Termersetzung für den OPAL-Compiler. TU Berlin (unveröffentlicht). 1990.

[Har 87] D. Harel. Statecharts: A visual formalsim for complex systems. SCP, 8:231-274, 1987.

[Hay 87] Ian Hayes (Ed.). Specification Case Studies. Prentice Hall, 1987.

[Heh 84] E.C.R. Hehner. Predicative programming, Part I and II. Comm. ACM, 27(2):134-151, 1984.

[HHP 87] R. Harper, F. Honsell, G. Plotkin. A Framework for Defining Logics. Proc. 2nd IEEE Symp. on Logic in Computer Science, Cornell, pp 194-204 (1987).

[HHS 93] C.A.R. Hoare, J. He, A. Sampaio. Normal form approach to compiler design. Acta Informatica 30 (1993) 701-739.

[Hoa 85a] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, London, 1985.

[Hoa 85b] C.A.R. Hoare. Programs are predicates. In C.A.R. Hoare and J.C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 141-155, Prentice-Hall, London, 1985.

[Hoo 91] J.J.M. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558 (Springer-Verlag, 1991).

[Hoo 94] J. Hooman. Correctness of Real Time Systems by Construction. In [LRV94}, 19-40.

[HP 88] Hatley, D. J.; Pirbhai, I. A.: Strategies for Real-Time System Specifications. Dorset House, New York (1988).

[HPPSS 87] D. Harel, A. Pnueli, J. Pruzan-Schmidt, and R. Sherman. On the formal semantics of Statecharts. In Proc. Symp. on Logic in Computer Science (1987) 54-64.

[Hu 91] Huizing, C.: Semantics of Reactive Systems: Comparison and Full Abstraction. Thesis, Technische Universiteit Eindhoven (1991).

[HZ 93] J. He and J. Zheng. Synchronous Circuit Realisation of Programs. ProCoS Document [OU HJF 16/1], Oxford University, 1993.

[INM 88] INMOS Ltd. OCCAM 2 Reference Manual. Prentice Hall, 1988.

[ISO 9000] DIN ISO 9000 Teil 3: Qualitätsmanagement- und Qualitätssicherungsnormen - Leitfaden für die Anwendung von ISO 9001 auf die Entwicklung, Lieferung und Wartung von Software. DIN, Deutsches Institut für Normung e.V., Beuth Verlag Berlin (1990).

[Klop 92] J.W. Klop: Term Rewriting Systems. Tech-Report CS-R9073, CWI, Amsterdam. Kurzfassung auch in: S. Abramski, Dov. M. Gabbay, T.S.E. Maibaum (eds): Handbook of Logic in Computer Science, Chapter 1. Oxford Science Publications, 1992.

[KP 92] Y.Kesten, A.Pnueli.: Timed and hybrid statecharts and their textual representation. In J.Vytopil (ed.): Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer (1992) 591-619.

[Lam 91] L. Lamport. The temporal Logic of Actions. DEC Systems Research Center, April 1991. Manuscript.

[LM 91] X. Leroy, M. Mauny: Dynamics in ML. in: J. Hughes (editor), Functional Programming Languages and Computer Architecture, 5th ACM Conference, Springer Verlag, LNCS 523, pp. 406-426, 1991.

[LP 92] Z. Luo and R. Pollack. Lego proof development system: User's manual. Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, May 1992.

[LRV 94] H. Langmaack, W.-P. de Roever, J. Vytopil (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863 (Springer-Verlag, 1994).

[LT 89] N.A. Lynch and M.R. Tuttle. An introduction to input/ouput automata. Technical Report CWI-Quarterly 2(3), CWI, 1989.

[Mey 94] Meyer, Th.: Generierung inkrementeller Evaluatoren für modulare und parametrisierte Attributierungen. Informatik Bericht, Universität Bremen (erscheint 1994)

[MM 93] N. Martí-Oliet, J. Meseguer: Rewriting-Logic as a Logic and Semantic Framework. Technical Report SRI-CSL-93-05, Computer Science Laboratory, SRI International, 1993.

[MP 91] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer-Verlag, 1991.

[MWW 84] U. Möncke, B. Weisgerber, R. Wilhelm: How to Implement a System for Manipulation of Attributed Trees, in: GI 8. Jahrestagung "Programmiersprachen und Programmentwicklung", Zürich, ed.: U. Ammann, pp 112-127, IFB vol. 77, Springer Verlag, 1984.

[NSY 91] X. Nicollin, J. Sifakis, S. Yovine. From ATP to Timed Graphs and Hybrid Systems. REX 1991, LNCS 600 (Springer-Verlag, 1991), 549-572.

[ORS 92] S. Owre, J. Rushby and N. Shankar. PVS: A prototype verification system. In 11th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 607 (Springer-Verlag, 1992) 748-752.

[Ous 93] J. K. Ousterhout: An Introduction to Tcl and Tk. Computer Science Division, Department of Eletrical Engineering and Computer Sciences, University of California, Berkeley, 1993.

[Ous 94] J. K. Ousterhout: Tcl und Tk. Addison Wesley. 1994.

[Paul 87] L.C. Paulson: Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.

[Paul 89] L.C. Paulson: The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363-397, 1989.

[Paul 95] L. Paulson: Isabelle: A generic theorem prover. LNCS 828, 1995.

[PW 94] Pepper, P., Wirsing, M. (eds.): KORSO: A Methodology for the Development of Correct Software. in [BJ 94].

[Rei 85] W. Reisig. Petri Nets - An Introduction. Springer-Verlag, 1985.

[Rei 94] W. Reif. The KIV approach to software verification: state of affairs and perspectives. In M. Broy, S. Jähnichen (Eds.), KORSO - Correct Software by Formal Methods, Project Report, 1994.

[Reis 90] S. Reis: Interacting with the FIELD Environment. in: Software Practice amd Experience, Vol 20, pp. 89-115, 1990.

[RRH 93] A.P. Ravn, H. Rischel, K.M. Hansen. Specifying and Verifying Requirements of Real-Time Systems. IEEE Transactions on Software Engineering, vol. 19,1 (1993) 41-55.

[Smi 85] D. R. Smith: The Design of Divide and Conquer Algorithms. Science of Computer Programming 5 (1985) 37-58.

[Smi 91] D. R. Smith: KIDS - a Knowledge-based Software Development System. In: M. M. Lowry, R. D. McCartney (eds.): Automating Software Design, Menlo Park, CA. AAAI Press / MIT-Press (1991) 483 - 514.

[Spi 89] J.M. Spivey. The Z Notation - A Reference Manual. Prentice Hall, 1989.

[Spi 89] J.M.Spivey: The Z Notation: A Reference Manual, Prentice-Hall, 1989.

[SS 94] J.U. Skakkebæk and N. Shankar. Towards a Duration Calculus Proof Assistant in PVS. In [LRV94}, 660-679.

[Sun 93] ToolTalk 1.2 User's Guide, Sun Microsystems Inc., 1993.

[SZH 94] D. Scholefield, H. Zehan, J. He. A Specification Oriented Semantics for the Refinement of Real-Time Systems, to appear in Theoretical Computer Science 1994.

[Talc 93] C. Talcott: A theory of binding structures and applications to rewriting. Theoretical Computer Science, 112 (1993) 99-143.

[VMOD] Der Bundesminister des Innern: Planung und Durchführung von IT-Vorhaben - Vorgehensmodell. KBSt, Koordinierungs- und Beratungsstelle der Bundesregierung für Informationstechnik in der Bundesverwaltung (1992).

[VSE 94] Ullmann, Hauff, Loevenich, Baur, Göhner, Kejwal, Reif, Stephan, Hutter, Sengler, Canver. VSE Verification Support Environment. Ein Wekzeug zur Entwicklung vertrauenswürdiger und zuverlässiger Systeme in Anlehnung an gültige Sicherheitskriterien. In Proc. 3. GI-Fachtagung Verläßliche Informationssysteme, VIS 93, München 1993.

[WM85] P.T. Ward and S.J. Mellor. Structured Development for Real-Time Systems. (3 vols), Yourdon Press Computing Series, Prentice-Hall, Englewood Cliffs, 1985.

[YWA 92] Y. Yang, J. Welsh, W. Allison: Supporting Multiple Tool Integration Paradigms Within a Single Environment, Software Verification Research Center, University of Queensland, 1992.

[ZHR 92] C. Zhou, C.A.R. Hoare, A.P. Ravn. A Calculus of Durations. IPL 40(5), 1992, 269-276.

8.2. Veröffentlichungen vor Beginn des Projekts

Dieser Abschnitt enthält eine für dieses Projekt relevante Auswahl von Veröffentlichungen der Antragsteller und ihrer Arbeitsgruppen vor Beginn des Projekts.

[AO 94] K.R. Apt, E.-R. Olderog. Programmverifikation - sequentielle, parallele und verteilte Programme (Springer-Verlag, 1994).

[B+ 85] Bauer, F.L., Berghammer, R., Broy, M., Dosch, W., Gnatz, R., Geiselbrechtinger, F., Hangel, E., Hesse, W., Krieg.-Brückner, B., Laut, A., Matzner, T.A., Möller, B., Nickl, F., Partsch, H., Pepper, P., Samelson, K., Wirsing, M., Wössner, H.: The Munich Project CIP, Vol. 1 : The Wide Spectrum Language CIP-L. LNCS 183, 1985.

[Bae 94] Baer, A.: RELIS 2000 - ein integrales Leit-, Informations- und Sicherungssystem für Regionalbahnen. VDI Berichte Nr. 1154, 1994.

[BH 94] J. Bohn and H. Hungar. TRAVERDI - Transformation and Verification of Distributed Systems. In M. Broy, S. Jähnichen (Eds.), KORSO - Correct Software by Formal Methods, Project Report, 1994.

[Boh 94] J. Bohn. Formalizing the SL/PL Transformational Approach in LAMBDA. Manuscript, Univ. Oldenburg, 1994.

[BW 94] David Basin and Toby Walsh. Termination orderings for rippling. In Proc. 12th International Conference On Automated Deduction (CADE-12), Nancy, France, June 1994. Springer-Verlag.

[FW 94] 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.

[FW 95] Fröhlich, M., Werner, M.: Demonstration of the interactive Graph-Visualization System daVinci. in: R. Tamassia, I. G. Tollis (eds.): Proc. DIMACS Workshop on Graph Drawing '94, Princeton. LNCS, (1995).

[Ger 92] Gersdorf, B.: Entwurf, formale Definition und Implementierung der funktional-logischen Programmiersprache ET. Dissertation, Universität Bremen, 1992.

[HHP 93] Hamer, Hörcher, Peleska: Safer Software - an Introduction into Formal Software Engineering. Technischer Report, DST (1993).

[HK 93] Hoffmann, B., Krieg-Brückner, B. (eds.): PROgram Development by Specification and Transformation, The PROSPECTRA Methodology, Language Family, and System. LNCS 680, 1993.

[HP 94] Hörcher, Peleska: The Role of Formal Specifications in Software Test. Tutorial at FME '94 (Formal Methods Europe Conf.).

[Karl 94a] E. W. Karlsen: Tool Integration in a Persistent Functional Setting. in [Kri 94a].

[Karl 94b] E. W. Karlsen: Higher Order Operating System Interfaces. in [Kri 94b].

[Karl 94c] E. W. Karlsen: Messenger - A Higher Order Message Broadcast Server, Technical Report, Universität Bremen, 1994.

[KBB 92] Ina Kraan, David Basin, and Alan Bundy. Logic program synthesis via proof planning. In K.K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation, pages 1-14. Springer-Verlag, 1993. Also available as Max-Planck-Institut für Informatik Research Paper MPI-I-92-244.

[KKLT 91] Krieg-Brückner, B., Karlsen, E.W., Liu, J., Traynor, O.: The PROSPECTRA Methodology and System: Uniform Transformational (Meta-) Development. in: Prehn, S., Toetenel, W. J. (eds.): VDM'91, Formal Software Development Methods; Vol. 2: Tutorials. LNCS 552 (1991) 363-397.

[KKT 92] Karlsen, E.W., Krieg-Brückner, B., Traynor, O.: The PROSPECTRA System: A Unified Development Framework. In: M.Nivat, C. Rattray, T. Rus, G. Scollo (ed.): Algebraic Methodology and Software Technology (AMAST'91), Workshop in Computing Springer-Verlag, London (1992) 421 - 433.

[Kle 94] S. Kleuker. Case Study: Stepwise Refinement of a Communication Processor Using Trace Logic. In: Proc. Semantics of Specification Languages, Workshops in Computing, (Springer-Verlag, 1994) 252-269.

[KLSW 94] Krieg-Brückner, B., Liu, J., Shi, H., Wolff, B.: Towards Correct, Efficient and Reusable Transformational Developments. in: Broy, M., Jähnichen, S. (eds.): KORSO, Correct Software by Formal Methods, LNCS (eingereicht) (erweiterte Fassung in [Kri 94a]).

[KLWS 93] Krieg-Brückner, B., Liu, J., Wolff, B., Shi, H.: Towards Correctness, Efficiency and Reusability of Transformational Developments. in: H. Reichel (ed.): Informatik - Wirtschaft - Gesellschaft, 23. GI Jahrestagung 1993, Dresden, Fachgespräch "Spezifikation und Semantik", Reihe Informatik Aktuell, Springer Verlag (1993) 241-252 (Extended Abstract).

[KM 94] Krieg-Brückner, B., Menzel, W. (eds.), Reif, W., Ruess, H., Santen, Th., Schwier, D., Schellhorn, G., Stenzel, K., Stephan, W.: System Architecture Framework for KORSO. in: Broy, M., Jähnichen, S. (eds.): KORSO, Correct Software by Formal Methods, LNCS (eingereicht) auch in [Kri 94a].

[Kri 90a] Krieg-Brückner, B.: PROgram development by SPECification and TRAnsformation. in: Technique et Science Informatiques Special Issue on Advanced Software Engineering in ESPRIT (1990) 134-149 (invited paper).

[Kri 90b] Krieg-Brückner, B.: COMPASS, a COMPrehensive Algebraic approach for System Specification and development, ESPRIT Basic Research Working Group 3264. EATCS Bulletin 40 (1990) 144-157.

[Kri 91] Krieg-Brückner, B.: Transformational Meta-Program Development. in: Broy, M., Wirsing, M. (eds.): Methods of Programming. LNCS 544 (1991) 19-34.

[Kri 94a] Krieg-Brückner, B. (Hrsg.): Programmentwicklung durch Spezifikation und Transformation - Bremer Beiträge zum Verbundprojekt KORSO (Korrekte Software). Informatik Bericht Nr. 1/94, Universität Bremen, 1994.

[Kri 94b] Krieg-Brückner, B. (Hrsg.): Programmentwicklung durch Spezifikation und Transformation - Bremer Beiträge zum Verbundprojekt KORSO (Korrekte Software); Band 2. Informatik Bericht Nr. 10/94, Universität Bremen, 1994.

[KS 91] Krieg-Brückner, B., Sannella, D.: Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL. Proc. TAPSOFT '91, LNCS 494 (1991) 313-336.

[KW 94] Karlsen, W., Wu, Y.: Incorporating Persistence in a Strictly Evaluated Purely Applicative Language. KORSO Bericht, in [Kri 94a].

[Liu 93] Liu, J.: A Semantic Basis for Logic-Independent Transformations. In F. Orejas (eds.): Proc. 9th WADT-COMPASS Workshop, LNCS 785 . auch in [Kri 94a].

[Liu 94] Liu, J.: Higher-Order Structured Presentations in a Logical Framework. Dissertation, Universität Bremen, 1994.

[LRV 94] H. Langmaack, W.-P. de Roever, J. Vytopil (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 863 (Springer-Verlag, 1994).

[MB 93] Sean Matthews, Alan Smaill, and David Basin. Experience with FS0 as a framework theory. In Gérard Huet and Gordon Plotkin, editors, Logical Environments, pages 61-82. Cambridge University Press, 1993.

[Old 91] E.-R. Olderog. Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge Tracts in Theoretical Computer Science 23. Cambridge University Press, 1991.

[Old 92] E.-R. Olderog. Interfaces between Languages for Communicating Systems. In W. Kuich, editor, Proc. ICALP 92}, Lecture Notes in Computer Science 623, pages 641-655. Springer-Verlag, 1992. invited paper.

[OR 93] E.-R. Olderog and S. Rössig. A case study in transformational design of concurrent systems. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT'93: Theory and Practice of Software Development, Lecture Notes in Computer Science 668, pages 90-104. Springer-Verlag, 1993.

[ORSS 92] E.-R. Olderog, S. Rössig, J. Sander, and M. Schenke. ProCoS at Oldenburg: The Interface between Specification Language and occam-like Programming Language. Technical Report Bericht 3/92, Univ. Oldenburg, Fachbereich Informatik, 1992.

[Pe 91] Peleska: Design and verification of fault tolerant systems with CSP. Distributed Computing (1991) 5:95-106.

[Pe 92] Peleska: Formale Methoden beim Entwurf ausfallsicherer, verteilter Systeme. In Lippold, Schmitz (ed.): Sicherheit in netzgestüzten Informationssystemen. Proceedings des BIFOA-Kongresses SECUNET '92, Vieweg (1992), pp. 293-308.

[Pe 93a] Peleska: CSP, Formal Software-Engineering and the Development of Fault-Tolerant Systems. In Vytopil (ed.): Formal Techniques in Real-Time and Fault-Tolerant Systems. Kluwer Academic Publishers (1993), pp. 167-207.

[Pe 93b] Peleska: Formales Software-Engineering mit strukturierten Methoden und Z: nachweisbare Korrektheit für sicherheits-relevante Anwendungen. In Scheibel (ed.): Software-Entwicklung - Methoden, Werkzeuge, Erfahrungen '93. Technische Akademie Esslingen (1993), pp.753-762.

[PH 94] Peleska, Hamer: The Airbus A330/340 Cabin Communication System - A Z Application. Technischer Report DST (1994) - erscheint in M. Hinchey (ed.) Formal Methods Case Studies, Prentice Hall (1995).

[PHP 94] Peleska, Huizing, Petersohn: A Comparison of Ward&Mellor's Transformation Schema with State-&Activitycharts. Vortrag auf BCS Sixth Refinement Workshop 1994. Computing Science Note 94/11, Eindhoven University of Technology (1994) - Zur Veröffentlichung eingereicht in IEEE Transactions on Software Engineering.

[PHPR 94] Petersohn, Huizing, Peleska, de Roever: Formal Semantics for Ward&Mellor's Transformation Schemas and the Specification of Fault-Tolerant Systems. Angenommener Vortrag zur EDCC-1, Berlin (1994).

[ProCoS 94] J. He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.-R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn and H. Rischel, Provably Correct Systems. In [LRV94], 288-335.

[Qian 94] Qian, Z.: Higher-Order Equational Logic Programming. In: Proc. 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (January 1994) 254-267.

[QW 92] Qian, Z. Kang, W.: Higher-Order E-Unification for Arbitrary Theories. in: Proc. Joint Int'l Conf. and Symp. on Logic Programming, MIT Press (1992) 52-66.

[Roe 94] S. Rössig. A Transformational Approach to the Design of Communicating Systems. Dissertation, Univ. Oldenburg, 1994.

[RS 91] S. Rössig and M. Schenke. Specification and stepwise development of communicating systems. In S. Prehn and W.J. Toetenel, editors, VDM'91 Formal Software Development Methods, LNCS 551, pages 149-163. Springer-Verlag, 1991.

[San 92] J. Sander. Entwicklung kommunizierender Programme aus Spezifikationen mit Hilfe der Expansions-Strategie. Diplomarbeit, Univ. Oldenburg, 1992.

[Sch 94a] M. Schenke. A Timed Specification Language for Concurrent Reactive Systems. In: Proc. Semantics of Specification Languages, Workshops in Computing, (Springer-Verlag, 1994) 152-167.

[Sch 94b] M. Schenke. Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency. In [LRV94], 605-620.

[Sch 94c] M. Schulte. Spezifikation und Verifikation von kommunizierenden Objekten in einem verteilten System. Diplomarbeit, Univ. Oldenburg, 1994.

[Shi 94a] Shi, H.: An Efficient Matching Algorithm for Convergent Rewrite Systems. Proc. 10th WADT-COMPASS Workshop, LNCS 1113 , 1994 (submitted).

[Shi 94b] Shi, H.: Extended Matching and Application to Program Transformation. Dissertation, Universität Bremen, 1994.

[Spr 94] A. Sprock. Entwicklung von Implementierungen regulärer und atomarer Register durch Transformationen. Diplomarbeit, Univ. Oldenburg, 1994.

[SW 93] Shi, H., Wolff, B.: Second-Order Matching with Matching Combinators. KORSO Bericht, 1993; in [Kri 94a].

[SW 94] Shi, H., Wolff, B.: A Finitary Matching Algorithm for Constructor Based Theories. KORSO Bericht, in [Kri 94a].

[Wang 94] Wang, K. : Higher-Order Constraint Logic Programming. Dissertation, Universität Bremen, 1994.

[Wolff 94] Wolff, B.: SPEC - A Unified Approach to Modularisation, Parametrisation, and Views in Attributations, KORSO Bericht, in [Kri 94b].

[WS 94] Wolff, B., Shi, H.: A Calculus of Transformation. KORSO Bericht, in [Kri 94b].

8.3. Veröffentlichungen im Rahmen des UniForM Projekts

In diesem Abschnitt sind neben Veröffentlichungen auch Arbeitsberichte des Projekts enthalten.

[Ast 95a] Auszug aus Kundenaufgabenstellung für Steuerung eingleisiger Strecken. Elpro LET GmbH, November 1995.

[Ast 95b] Aufgabenstellung für Steuerung eingleisiger Strecken. Elpro LET GmbH, November 1995.

[AKK 96] Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B.(eds.): Algebraic Foundations of System Specification. (in preparation).

[Be 95a] Untersuchungen zu den Einsatzmöglichkeiten der SPS-Programmiersprache ST. Arbeitsbericht zum Projekt UniForM Workbench. Elpro LET GmbH, August 1995.

[Be 95b] Untersuchungen zu den Einsatzmöglichkeiten der SIMATICS S7. Arbeitsbericht zum Projekt UniForM Workbench. Elpro LET GmbH, September 1995.

[Be 95a] Bericht zum Einsatz des Testprogramms SIMPRO am Beispiel der Testung eines BÜ-Programms. Arbeitsbericht zum Projekt UniForM Workbench. Elpro LET GmbH, Dezember 1995.

[BJ 96] J. Bohn, W. Janssen: A strategic approach to transformational design. In: M.-C. Gaudel, J. Woodcock (eds.): FME'96: Industrial Benefit and Advances in Formal Methods. LNCS 1051 (1996) 609-628.

[BK 96] Basin, D., Krieg-Brückner, B.: Formalization of the development process. Chapter 13 in Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B.(eds.): Algebraic Foundations of System Specification. (in preparation).

[BR 95] J. Bohn, S. Rössig: On automatic and interactive design of communicating systems. In: E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, B. Steffen (eds.): Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019 (1995) 216--247.

[CQS 96] R. Curien, Z. Qian, H. Shi: Efficient Second-Order Matching. Proc. 7th Int'l Conf. on Rewriting Techniques and Applications. LNCS 1996 (to appear).

[Dick 95] Dick, S.: Systemanforderungen an eine Simulationsumgebung für FDR. UniForM Bericht, Universität Bremen, 1995.

[K+ 95] Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Balzer, D., Baer, A.: Universelle Entwicklungsumgebung für Formale Methoden (UniForM Workbench). Informatik Bericht Nr. 8/95, Universität Bremen, 1995.

[K+ 96] Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Balzer, D., Baer, A.: UniForM, Universal Formal Methods Workbench. in Grote, U. (ed.): Statusseminar Softwaretechnologie. BMBF (to appear).

[KLSW 95] Krieg-Brückner, B., Liu, J., Shi, H., Wolff, B.: Towards Correct, Efficient and Reusable Transformational Developments. in: Broy, M., Jähnichen, S. (eds.): KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Final Report. Lecture Notes in Computer Science 1009 (1995) 270-284.

[KSW 96] Kolyang, T. Santen, B. Wolff: Correct and User-Friendly Implementations of Transformation Systems. In: M.-C. Gaudel, J. Woodcock (eds.): FME'96: Industrial Benefit and Advances in Formal Methods. LNCS 1051 (1996) 629-648. http://www.informatik.uni-bremen.de/~bu/papers/yats.ps.gz

[KW 95] Kolyang, B. Wolff: Development by Refinement Revisited: Lessons learnt from an Example. Proc. Softwaretechnik '95, Braunschweig. Erschienen in Softwaretechnik Trends, Bd. 15, Heft 3, ISSN 0720-8928, Oktober 1995.

[ORS 96] E.-R. Olderog, A.P. Ravn, J.U. Skakkebæk: Refining System Requirements to Program Specifications, in: C. Heitmeyer and D. Mandrioli (Eds.): Formal Methods in Real-Time Systems, Trends in Software-Engineering, Chapt. 5, Wiley, 1996.

[OS 95] E.-R. Olderog, Michael Schenke: Design of Real-Time Systems: Interface between Duration Calculus and Program Specifications. In: J. Desel (Ed.): Structures in Concurrency Theory, Workshops in Computing (1995) 32-54.

[Pel 96a] J. Peleska: Formal Methods and the Development of Dependable Systems. Bericht 1/96, Universität Bremen, Fachbereich Mathematik und Informatik (1996) 72p. http://www.inormatik.uni-bremen.de/~jp/papers/depend.ps.gz

[Pel 96b] J. Peleska: 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.

[PS 96] J. Peleska, M. Siegel: 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.

[SD 95] Th. Santen, S. Dick: Searching for a Global Search Algorithm. Proc. 10th Knowledge Based Software Engineering Conf. KBSE '95, Boston Mass., IEEE Computer Society Press (1995).

[Shi 96] H. Shi: A Semantic Matching Algorithm: Analysis and Implementation. Proc. 21st Int'l Symp. on Mathematical Foundations of Computer Science. LNCS 1996 (to appear).

[SIMPRO] Testprogramm SIMPRO. Elpro LET GmbH, Oktober 1995.