Publications 1998-2000

 

4 Publications 1998-2000 (with Abstracts)

[Weh00a]

H. Wehrheim. Data Abstraction Techniques in the Validation of CSP-OZ Specifications. Formal Aspects of Computing, 12, 2000.
[ bib ]

[DT00]

H. Dierks and J. Tapken. Modelling and Verifying of `Cash-Point Service' Using Moby/PLC. Formal Aspects of Computing, 12:222-221, 2000.
[ bib | .ps.gz ]

[OR00]

E.-R. Olderog and A.P. Ravn. Documenting design refinement. In M.P.E. Heimdahl, editor, Proc. of the Third Workshop on Formal Methods in Software Practice, pages 89-100. ACM, 2000.
[ bib | .ps ]

We show how UML class diagrams can be used to document design by refinement in the early design stages. This is illustrated by an example from the area of embedded real-time and hybrid systems. A precise semantics is given for the UML class diagrams by translation to the Z schema calculus.

[FW00a]

Clemens Fischer and Heike Wehrheim. Behavioural Subtyping Relations for Object-Oriented Formalisms. In T. Rus, editor, Algebraic Methodology and Software Technology, volume 1816 of LNCS, pages 469-483. Springer, 2000.
[ bib | .ps ]

In this paper we investigate the object-oriented notion of subtyping in the context of behavioural formalisms. Subtyping in OO-formalisms is closely related to the concept of inheritance. The central issue in the choice of subtyping relations among classes is the principle of substitutability: an instance of the subtype should be usable wherever an instance of the supertype was expected. Depending on the interpretation of ``usable'', we obtain a variety of subtyping relations: stronger subtyping relations, allowing one to share the subtype instance among different clients without any change compared with the supertype, and weaker relations, restricting the possibilities of interference of different clients on the subtype instance. The subtyping relations are taxonomically ordered in a hierarchy. The concept of ``usability'' is formalised via testing scenarios, which provide alternative characterisations for the subtyping relations.

[Weh00c]

Heike Wehrheim. Specification of an automatic manufacturing system - a case study in using integrated formal methods. In FASE 2000, Fundamental Approaches to Software Engineering, volume 1783 of LNCS, 2000.
[ bib | .ps ]

An automatic manufacturing system serves as a case study for the applicability of an integrated formal method to the specification of software systems. The formal method chosen is CSP-OZ, an integration of the state-oriented formalism Object-Z with the process algebra CSP. The practicability as well as limitations of CSP-OZ are studied. We furthermore employ a graphical notation (class diagrams) from the Unified Modelling Language to describe the architectural view of the system. The correctness of the obtained specification is checked by a translation into the input language of the CSP model checker FDR and a following property check.

[Die00b]

H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata . Theoret. Comput. Sci., 253(1):61-93, December 2000. full version of [?].
[ bib ]

[Die00a]

H. Dierks. A Process Algebra for Real-Time Programs. In T. Maibaum, editor, FASE 2000: Fundamental Approaches to Software Engineering, volume 1783 of Lecture Notes in Computer Science, pages 66-81. Springer-Verlag, 2000.
[ bib ]

[Die00c]

H. Dierks. Specification and Verification of Polling Real-Time Systems. In H. Fiedler, O. Günther, W. Grass, S. Hölldobler, G. Hotz, R. Reischuk, B. Seeger, and D. Wagner, editors, Ausgezeichnete Informatikdissertationen 1999. Teubner, 2000.
[ bib | .ps.gz ]

[Bre00]

Jan Bredereke. Families of formal requirements in telephone switching. In Feature Interactions in Telecommunications and Software Systems VI, Amsterdam, May 2000. IOS Press. Submitted. An abstract is available here.
[ bib ]

[Weh00b]

Heike Wehrheim. Behavioural subtyping and property preservation. In S. Smith and C. Talcott, editors, FMOODS'00: Formal Methods for Open Object-Based Distributed Systems. Kluwer, 2000.
[ bib | .ps ]

Inheritance is one of the key features in object-oriented design and analysis. It especially supports an incremental development by allowing to stepwise add new functionality to an existing system design. When using a subclass which is a specialisation of a certain superclass, the question arises which of the superclass' properties still hold for the subclass. We investigate this topic for three behavioural subtyping relations, which formalise the subtype - supertype relationship among classes on the basis of process algebra correctness relations. According to the degree of change allowed by the subtyping relations, safety and liveness properties of the superclass are preserved up to different extents.

[Weh00d]

Heike Wehrheim. Subtyping patterns for active objects. In H. Giese and S. Philippi, editors, Proceedings 8ter Workshop des GI-Arbeitskreises GROOM: Visuelle Verhaltensmodellierung verteilter und nebenläufiger Software-Systeme. Universität Münster, 2000. No. 24/00-I.
[ bib ]

[FW00b]

Clemens Fischer and Heike Wehrheim. Failure-divergence semantics as a formal basis for an object-oriented integrated formal method. Bulletin of the EATCS (European Association of Theoretical Computer Science), 71:92 - 101, 2000.
[ bib | .ps ]

The integration of several different modelling techniques into a single formal method has turned out to be advantageous in the formal design of software systems. Giving a semantics to an integrated formal method is currently a very active area of research. In this paper we discuss the advantages of a failure-divergence semantics for data and process integrating formal methods, in particular for those with a concept of inheritance. The discussion proceeds along the lines of the formal method CSP-OZ, a combination of CSP and Object-Z, developed in Oldenburg.

[SD99]

M. Schenke and M. Dossis. Provably correct hardware compilation using timing diagrams. In FORTE/PSTV'99, pages 313-331. Kluwer, 1999.
[ bib ]

[SL99]

M. Schenke and A. Lavrov. Automata-based stochastic analysis of modular hybrid controllers. In Conference on Probabilistic Analysis of Rare Events (RARE), 1999. ISBN 9984-668-08-8.
[ bib ]

[KBPOB99]

B. Krieg-Brückner, J. Peleska, E.-R. Olderog, and A. Baer. The UniForM Workbench, a Universal Development Environment for Formal Methods. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM'99 - Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1186-1205. Springer, 1999.
[ bib ]

[ER99]

E.-R.Olderog. Sichere Bahnsteuerungen. Log IN, (1):64-65, 1999.
[ bib ]

[Old99a]

E.-R. Olderog. Correct Real-Time Software for Programmable Logic Controllers. In Correct System Design - Recent Insights and Advances, volume 1710 of Lecture Notes in Computer Science, pages 342-362. Springer, 1999.
[ bib ]

[Old99b]

E.-R. Olderog. Entwicklung korrekter zeitkritischer Systeme. In K. Spies and B. Schätz, editors, Formale Beschreibungstechniken für verteilte Systeme, volume 9 of GI/ITG Fachgespräch, pages 7-16. Utz Verlag, 1999.
[ bib ]

[ABB⁺99]

Joanne Atlee, Wolfram Bartussek, Jan Bredereke, Martin Glinz, Ridha Khedri, Lutz Prechelt, and David Weiss. Requirements. In Ernst Denert, Daniel Hoffman, Jochen Ludewig, and David Parnas, editors, Software Engineering Research and Education: Seeking a new Agenda, number 230 in Dagstuhl-Seminar-Report, ISSN 0940-1121, pages 9-16, Feb. 1999.
[ bib ]

[BFK⁺99]

Jan Bredereke, Karol Frühauf, Ridha Khedri, Stefan Krauß, and Andreas Zeller. Maintenance. In Ernst Denert, Daniel Hoffman, Jochen Ludewig, and David Parnas, editors, Software Engineering Research and Education: Seeking a new Agenda, number 230 in Dagstuhl-Seminar-Report, ISSN 0940-1121, pages 41-43, Feb. 1999.
[ bib ]

[Bre99a]

Jan Bredereke. Maintaining telephone switching software requirements. IEEE Communications Magazine, 1999. Submitted. An abstract is available here.
[ bib ]

[Bre99c]

Jan Bredereke. Modular, changeable requirements in functional documentation for telephone switching. Formal Methods in System Design, 1999. Special issue on Tabular Notation. Submitted. An extended abstract is available here.
[ bib ]

[Bre99b]

Jan Bredereke. Maintaining telephone switching system requirements. In Participants' notes of Dagstuhl seminar 99071 - software engineering research and education: seeking a new agenda, 15-19 Feb. 1999.
[ bib ]

[FW99]

Clemens Fischer and Heike Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway, and K. Taguchi, editors, Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pages 315-334. Springer, 1999.
[ bib | .ps.gz ]

CSP-OZ is a formal method integrating two different specifications formalisms into one: the formalism Object-Z for the description of static aspects, and the process algebra CSP for the description of the dynamic behaviour of systems. The semantics of CSP-OZ is failure divergence taken from the process algebra side. In this paper we propose a method for checking correctness of CSP-OZ specifications via a translation into the CSP dialect of the model checker FDR.

[Tap99]

Josef Tapken. Implementing Hierarchical Graph-Structures. In J.-P. Finance, editor, Proceedings of FASE'99, volume 1577 of LNCS, pages 219-233. Springer-Verlag, 1999. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[Fis99]

Clemens Fischer. Software development with Object-Z, CSP and Java: A pragmatic link from formal specifications to programs. In B. Jacobs, B. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs, volume 251 of Technical Report, pages 29-35. Fernuniversität Hagen, 1999.
[ bib | .ps.gz ]

[SO99]

Michael Schenke and E.-R. Olderog. Transformational design of real-time systems - part 1: from requirements to program specifications. Acta Informatica 36, pages 1-65, 1999.
[ bib | .ps.gz ]

[Sch99]

Michael Schenke. Transformational design of real-time systems - part 2: from program specifications to programs. Acta Informatica 36, pages 67-99, 1999.
[ bib ]

[Die99]

H. Dierks. Synthesizing Controllers from Real-Time Specifications. IEEE Transactions on Computer-Aided Design of Integrated Circu its and Systems, 18(1):33-43, 1999.
[ bib | .ps.gz ]

[Bre98]

Jan Bredereke. Specification style and efficiency in Estelle. In Stanislaw Budkowski, Stefan Fischer, and Reinhard Gotzhein, editors, Proc. of the 1st Int'l. Workshop on the Formal Description Technique Estelle - Estelle'98, pages 165-186, Evry, France, 2 Nov. 1998. Institut National des Télécommunications.
[ bib | .ps.gz ]

[Old98]

E.-R. Olderog. Formal methods in real-time systems. In Proceedings of the 10th EuroMicro Workshop on Real Time Systems, pages 254-263. IEEE Computer Society, June 1998.
[ bib ]

[DFMV98]

H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In FTRTFT'98, Lecture Notes in Computer Science, pages 29-40. Springer-Verlag, 1998. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[Die98]

H. Dierks. Comparing Model-Checking and Logical Reasoning for Real-Time Systems. In ESSLLI'98, August 1998. Workshop proceedings.
[ bib | .ps.gz ]

[RR98]

A.P. Ravn and H. Rischel, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer Science, Lyngby, Denmark, September 1998. Springer-Verlag.
[ bib ]

[Tap98]

J. Tapken. Moby/PLC - A Design Tool for Hierarchical Real-Time Automata. In E. Astesiano, editor, Proceedings of FASE'98, volume 1382 of LNCS, pages 326-329. Springer Verlag, 1998.
[ bib ]

[TD98]

J. Tapken and H. Dierks. Moby/PLC - Graphical Development of PLC-Automata. In A.P. Ravn and H. Rischel, editors, Proceedings of FTRTFT'98, volume 1486 of LNCS, pages 311-314. Springer Verlag, 1998. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[FM98]

Clemens Fischer and D. Meemken. JaWA: Java with assertions. In C. H. Cap, editor, Java-Informations-Tage, Informatik aktuell, pages 49-59. Springer, 1998. In german.
[ bib ]

Methoden zur Entwicklung von korrekter Software und deren Einführung in die Praxis stellen heute immer noch ein schwieriges Problem dar.

Bertrand Meyer hat unter dem Stichwort 'Programmieren mit Vertrag' einen Vorschlag gemacht und durch Eiffel implementiert, wie man formale Spezifikationsanteile mit Programmcode mischen und zur Laufzeit überprüfen kann.

In diesem Paper geben wir einen Überblick über die Sprache JaWA, mit der dieses Konzept auf Java übertragen wurde.

JaWA Programme bestehen aus herkömmlichem Java-Code, der Zusicherungen (Invarianten, Vor- und Nachbedingungen) in Form von Kommentaren enthält. Der JaWA-Präcompiler übersetzt JaWA in Java. Er erzeugt zusätzliche Bedingungen, mit denen die spezifizierten Eigenschaften zur Laufzeit überprüft werden können. Dabei wird die Java Ausnahmebehandlung ausgenutzt und um Eiffel ähnliche `rescue' und `retry' Anweisungen ergänzt. Die erzeugten Fehlermeldungen und Warnungen sind frei konfigurierbar.

[Fis98]

Clemens Fischer. How to combine Z with a process algebra. In J. Bowen, A. Fett, and M. Hinchey, editors, ZUM'98 The Z Formal Specification Notation, volume 1493 of LNCS, pages 5-23. Springer, 1998.
[ bib ]

The specification language Z has been designed to describe data and functional aspects of systems, but it does not define a semantics for specifications in a distributed setting. Process algebras, on the other hand, concentrate on the behaviour of communicating agents. For this reason the combination of Z with a process algebra recently got a lot of attention. In this paper we summarise and categorise the different approaches and identify pitfalls and shortcomings in existing combinations. Thereby we give an overview over the many possible answers to the question: `What is the behavioural semantics of a Z specification?'

[Kle98]

S. Kleuker. Reengineering of distributed systems using formal methods. In P. Nesi and F. Lehner, editors, Proceedings of the Second Euromicro Conference on Software Maintenance and Reengineering, pages 189-192. IEEE Computer Society, 1998.
[ bib ]

[DS98]

H. Dierks and M. Schenke. A Unifying Framework for Correct Program Construction. In J. Jeuring, editor, Mathematics of Program Construction 98, volume 1422 of Lecture Notes in Computer Science, pages 122-150. Springer-Verlag, June 1998. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[DT98]

H. Dierks and J. Tapken. Tool-Supported Hierarchical Design of Distributed Real-Time Systems. In Euromicro Workshop on Real Time Systems, pages 222-229. IEEE, 1998.
[ bib | .ps.gz ]

[OD98]

E.-R. Olderog and H. Dierks. Decomposing Real-Time Specifications. In H. Langmaack, A. Pnueli, and W.P. de Roever, editors, Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science, pages 465-489. Springer-Verlag, 1998. An abstract is available on-line.
[ bib ]