Publications 2001-2003

 

3 Publications 2001-2003 (with Abstracts)

[RW03]

H. Rasch and H. Wehrheim. Checking Consistency in UML Diagrams: Classes and State Machines. In E. Najm, U. Nestmann, and P. Stevens, editors, Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 229-243. Springer, 2003.
[ bib | .ps ]

[Weh03b]

H. Wehrheim. Inheritance of Temporal Logic Properties. In E. Najm, U. Nestmann, and P. Stevens, editors, Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 79-93. Springer, 2003.
[ bib | .ps ]

[OW03]

E.-R. Olderog and H. Wehrheim. Specification and Inheritance in CSP-OZ. In F. de Boer, M. Bosangue, S. Graf, and W.-P. de Roever, editors, Formal Methods for Components and Objects, volume 2852 of LNCS, pages 361-379. Springer, 2003.
[ bib ]

CSP-OZ [Fis97,Fis00] is a combination of Communicating Sequential Processes (CSP) and Object-Z (OZ). It enables the specification of systems having both a state-based and a behaviour-oriented view using the object-oriented concepts of classes, instantiation and inheritance. CSP-OZ has a process semantics in the failures divergence model of CSP. In this paper we explain CSP-OZ and investigate the notion of inheritance. Behavioural subtyping relations between classes introduced in [Weh02] guarantee the inheritance of safety and ``liveness'' properties.

References

[Fis97]

C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), volume 2, pages 423-438. Chapman & Hall, 1997.

[Fis00]

C. Fischer. Combination and Implementation of Processes and Data: From CSP-OZ to Java. PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

[Weh02]

H. Wehrheim. Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation Thesis, 2002.

[SBB⁺03]

C. Schulte, M. Brörkens, I. Brückner, R. Buschermöhle, and T. Wolf. Sicherheit für sicherheitskritische Systeme. Electronic Embedded Systeme, pages 19-21, September 2003.
[ bib | .pdf ]

Mikroprozessoren werden immer häufiger auch in technischen Geräten und vielerlei alltäglichen Konsumgütern eingesetzt. Letzere werden auch als eingebettete Systeme bezeichnet, das heißt in umgebende technische Systeme wechselseitig integrierte Computersysteme. Die Entwicklung solcher eingebetteter Systeme wird unter anderem aufgrund immer höherer Anforderungen an die Funktionalität und einer wachsenden Anzahl von interagierenden Komponenten immer komplexer. Um diesem Umstand Rechnung zu tragen, werden in Prozessmodellen und Standards, die insbesondere im Bereich sicherheitskritischer Systeme angewendet werden, bereits seit geraumer Zeit vollständige Korrektheitsnachweise gefordert. Ein aussichtsreicher Kandidat in diesem Kontext ist das Model-Checking.

[Weh03a]

H. Wehrheim. Behavioral Subtyping Relations for Active Objects. Formal Methods in System Design, 23(2):143-170, 2003.
[ bib ]

[DW03]

J. Derrick and H. Wehrheim. Using coupled simulations in non-atomic refinement. In D. Bert, J. Bowen, S. King, and M. Walden, editors, ZB 2003: Formal Specification and Development in Z and B, volume 2651 of LNCS, pages 127-147. Springer, 2003.
[ bib | .ps ]

[Sch03]

A. Schäfer. Combining real-time model-checking and fault tree analysis. In D. Mandrioli, K. Araki, and S. Gnesi, editors, FM 2003: the 12th International FME Symposium, volume 2805 of LNCS, pages 522-541. Springer, 2003. This publication is available at SpringerLink.
[ bib | .pdf ]

We present a semantics for fault tree analysis, a technique used for the analysis of safety critical systems, in the real-time interval logic Duration Calculus with Liveness and show how properties of fault trees can be checked automatically. We apply this technique in two examples and show how it can be connected to other verification techniques.

[DT03]

H. Dierks and J. Tapken. Moby/DC - A tool for model-checking parametric real-time specifications. In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), volume 2619 of LNCS, pages 271-277. Springer, 2003.
[ bib | .ps.gz ]

We define an operational subset of Duration Calculus, called phase automata, which serves as an intermediate language for the analysis and verification of real-time system descriptions that contain timing parameters. We introduce the tool Moby/DC which implements a model-checking algorithm for phase automata. The algorithm applies compositional model-checking techniques and handles parameters by built-in procedures or by a link to CLP(R). Due to the parameters the model-checking problem is undecidable in general. Hence, we have to accept that the results are overapproximations only in order to guarantee termination. The overapproximation together with the compositional technique makes the model-checker especially well suited for proving the absence of error traces instead of finding them.

[OD03]

E.-R. Olderog and H. Dierks. Moby/RT: A Tool for Specification and Verification of Real-Time Systems. Journal of Universal Computer Science, 9:88-105, 2003.
[ bib ]

The tool Moby/RT supports the design of real-time systems at the levels of requirements, design specifications and programs. Requirements are expressed by constraint diagrams [Kle00], design specifications by PLC-Automata [Die00], and programs by Structured Text, a programming language dedicated for programmable logic controllers (PLCs), or by programs for LEGO Mindstorm robots. In this paper we outline the theoretical background of Moby-RT by discussing its semantic basis and its use for automatic verification by utilising the model-checker UPPAAL.

References

[Kle00]

Kleuker, C. (2000). Constraint Diagrams. PhD thesis, University of Oldenburg.

[Die00]

Dierks, H. (2000). PLC-Automata: A New Class of Implementable Real-Time Automata. TCS, 253(1):61-93.

[DO03]

H. Dierks and E.-R. Olderog. Temporale Spezifikationslogiken. at-Automatisierungstechnik, 51(2):A1-A4, 2003.
[ bib ]

Logiken sind in der Informatik ein weitverbreitetes Mittel zur Spezifikation. Dazu werden Logiken verschiedener Ausprägung benutzt, z.B. temporale Logiken für reaktive Systeme, zu denen die Systeme der Automatisierungstechnik zählen. Dieser Beitrag enthält eine Einführung in die wichtigsten temporalen Logiken und Literaturverweise.

English
Logics are often used in computer science as specification languages. There is a rich variety of logics to choose from depending on the problem. Systems in automation technology are typically reactive systems for which temporal logics are adequate. We introduce the most important temporal logics and give reference for further reading.

[Weh02b]

H. Wehrheim. Relating state-based and behaviour-oriented subtyping. Nordic Journal of Computing, 9(4):405-435, 2002. appeared March 2003.
[ bib ]

Subtyping relations for object-oriented formalisms describe relationships between classes which satisfy the substitutability requirement imposed on types and their subtypes. Subtyping relations have been proposed both for state-based and for behaviour-oriented specification formalisms. In this paper we state and proof correspondence results between these two forms of subtyping: starting from a state-based specification language we show that via a behaviour-oriented semantics state-based subtyping induces behaviour-oriented subtyping. In the comparison we study three different kinds of subtyping achieving substitutivity to a different degree. For all three kinds of definitions a correspondence result can be shown.

[HO02b]

J. Hoenicke and E.-R. Olderog. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing, 9(4):301-334, 2002. appeared March 2003.
[ bib ]

CSP-OZ-DC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. This combination is illustrated by specifying the train controller of a case study on radio controlled railway crossings. The technical contribution of the paper is a smooth integration of the underlying semantic models and its use for verifying timing properties of CSP-OZ-DC specifications. This is done by combining the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for timed automata with a new tool f2u that transforms FDR transition systems and certain patterns of Duration Calculus formulae into timed automata. This approach is illustrated by the example of a vending machine.

References

[BLL97]

J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and Wang Yi. Uppaal - a tool suite for automatic verification of real-time systems. In R. Alur, T.A. Henzinger, and E.D. Sonntag, editors, Hybrid Systems III - Verification and Control, volume 1066 of LNCS, pages 232-243. Springer, 1997.

[Hoa85]

C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[Ros94]

A.W. Roscoe. Model-checking CSP. In A.W. Roscoe, editor, A Classical Mind - Essays in Honour of C.A.R.Hoare, pages 353-378. Prentice-Hall, 1994.

[Smi00]

G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.

[ZHR91]

C. Zhou, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269-276, 1991.

[DBL02]

H. Dierks, G. Behrmann, and K.G. Larsen. Solving Planning Problems Using Real-Time Model-Checking (Translating PDDL3 into Timed Automata). In F. Kabanza and S. Thiebaux, editors, AIPS-Workshop Planning via Model-Checking, pages 30-39, April 2002.
[ bib | .ps.gz ]

[RW02]

H. Rasch and H. Wehrheim. Consistency between UML classes and associated state machines. In L. Kuzniarz, G. Reggio, J. L. Sourrouille, and Z. Huzar, editors, UML 2002 - Workshop on Consistency Problems in UML-based Software Development, volume 06, pages 46-60, 2002.
[ bib ]

[DL02]

H. Dierks and M. Lettrari. Constructing Test Automata from Graphical Real-Time Requirements. In FTRTFT 2002, Lecture Notes in Computer Science, pages 433-453. Springer-Verlag, September 2002.
[ bib | .ps.gz ]

[BM02a]

M. Brörkens and M. Möller. Dynamic Event Generation for Runtime Checking using the JDI. In Klaus Havelund and Grigore Rosu, editors, Proceedings of the Second Workshop on Runtime Verification (RV'02), Copenhagen, Denmark, July 2002, volume 70 of Electronic Notes in Theoretical Computer Science. Elsevier Science, July 2002. This publication is available at ENTCS.
[ bib | .pdf ]

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level - either by inserting new source code prior to the compilation or by modifying the target code, e.g. Java byte code, before running the program. The jassda framework and tool enable runtime checking of Java programs against a CSP-like specification. For generating events it uses the Java Debug Interface (JDI) and thus no modifications to the code are necessary. Another advantage is that events are generated on demand, i.e. dynamically at runtime it is determined which events to generate for the current debug run without modifying the program itself. This paper shows how this event generation is done by the jassda framework.

[HO02a]

J. Hoenicke and E.-R. Olderog. Combining Specification Techniques for Processes Data and Time. In M. Butler, L. Petre, and K. Sere, editors, Integrated Formal Methods, volume 2335 of Lecture Notes in Computer Science, pages 245-266. Springer-Verlag, May 2002.
[ bib | .pdf ]

We present a new combination CSP-OZ-DC of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. The emphasis is on a smooth integration of the underlying semantic models and its use for verifying properties of CSP-OZ-DC specifications by a combined application of the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for Timed Automata. This approach is applied to part of a case study on radio controlled railway crossings.

[M02]

Michael Möller. Specifying and Checking Java using CSP. In Workshop on Formal Techniques for Java-like Programs - FTfJP'2002. Computing Science Department, University of Nijmegen, June 2002. Technical Report NIII-R0204.
[ bib | .pdf ]

Currently several approaches are done in applying formal techniques to the Java programming language. A new trend is to take dynamic behaviour into account when designing such techniques. To bring formal techniques to practical applications one often has to reduce the goal coming down from full verification to runtime checking. jassda is a framework for performing such runtime checks at the byte-code level of Java. The Trace-Checker module of jassda allows one to test the dynamic behaviour of multiple Java virtual machines by monitoring whether the trace of all relevant events is a member of the trace semantics of a given CSP process or not. In this paper we present the CSP dialect that is used to specify a set of allowed traces for Java programs. The underlying semantics allows partial specifications of distributed Java programs and to recombine them while preserving properties.

[Weh02a]

H. Wehrheim. Checking behavioural subtypes via refinement. In B. Jacobs and A. Rensink, editors, FMOODS 2002: Formal Methods for Open Object-Based Distributed Systems, pages 79-93. Kluwer, May 2002.
[ bib | .ps ]

Behavioural subtyping is concerned with the question of whether one class is behaviourally consistent with another class. The word ``behaviour'' in this context usually refers to the semantics of methods, typically given by pre- and postconditions. In this paper, we will use this term in a more specific way, referring to the dynamic behaviour of objects in time. Behaviour descriptions of classes give sequencing constraints on method invocations, in this paper formulated using the process algebra CSP. Behavioural subtyping can be seen as a mixture of refinement and inheritance: we expect the subtype to be substitutable for the supertype while at the same moment allowing extension of functionality. Since refinement itself does not allow extension of functionality, a subtyping definition must therefore extend standard refinement concepts to cope with additional methods in the subtype. In this paper, we show for three such subtyping relations how they can, despite these extensions, be checked via refinement. This gives us the possibility of employing standard refinement checkers for CSP (viz. the FDR modelchecker) for subtype checks.

[BM02b]

M. Brörkens and M. Möller. jassda Trace Assertions. In Ina Schieferdecker, Hartmut König, and Adam Wolisz, editors, Trends in Testing Communicating Systems, International Confernece on Testing Communicating Systems (TestCom), pages 39-48, Berlin, Germany, March 2002.
[ bib | .pdf ]

[RW01]

A. Rensink and H. Wehrheim. Process algebra with action dependencies. Acta Informatica, (38):155-234, 2001.
[ bib ]

[Weh01]

Heike Wehrheim. Patterns and Rules for Behavioural Subtyping. In M. Kim, B. Chin, S. Kang, and D. Lee, editors, FORTE 2001, pages 335 - 352. Kluwer, 2001.
[ bib | .ps ]

Subtyping relations for object-oriented formalisms describe relationships between super- and subclasses which satisfy the substitutability requirement imposed on types and their subtypes. Behavioural subtyping is concerned with subtypes for active classes with an explicit dynamic behaviour, specifiable for instance by object-oriented formal methods combining state-based with behavioural formalisms. Such specification languages often have a formal semantics that composes behavioural semantics for both the behaviour and the state-based part. In this paper we develop syntactic patterns and semantic rules for the state-based part of a subclass which guarantee that the subclass is a behavioural subtype of its superclass. This allows to check for subtypes without computing the behavioural semantics of the class at all. Our results are similar to the ones linking data refinement in state-based methods with failure-divergence refinement in CSP. In contrast to classical data refinement, subtyping (and the simulation relations used for showing the soundness of the patterns) have to cope with additional new operations in the subclass.

[Hoe01]

J. Hoenicke. Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC. FBT 2001, June 2001.
[ bib | .ps ]

[BFMW01]

D. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim. Jass - Java with Assertions. In Klaus Havelund and Grigore Rosu, editors, Proceedings of the First Workshop on Runtime Verification (RV'01), Paris, France, July 2001, volume 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001. This publication is available at ENTCS.
[ bib | .pdf ]

Design by Contract, proposed by Meyer for the programming language Eiffel, is a technique that allows run-time checks of specification violation and their treatment during program execution. , Java with assertions, is a Design by Contract extension for Java allowing to annotate Java programs with specifications in the form of assertions. The tool is a pre-compiler that translates annotated into pure Java programs in which compliance with the specification is dynamically tested. Besides the standard Design by Contract features known from classical program verification (e.g. pre- and postconditions, invariants), additionally supports refinement, i.e. subtyping, checks and the novel concept of trace assertions. Trace assertions are used to monitor the dynamic behaviour of objects in time.

[FOW01]

C. Fischer, E.-R. Olderog, and H. Wehrheim. A CSP view on UML-RT structure diagrams. In H. Husmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lecture Notes in Computer Science, pages 91-108. Springer-Verlag, 2001.
[ bib | .ps ]

UML-RT is an extension of UML for modelling embedded reactive and real-time software systems. Its particular focus lies on system descriptions on the architectural level, defining the overall system structure. In this paper we propose to use UML-RT structure diagrams together with the formal method CSP-OZ combining CSP and Object-Z. While CSP-OZ is used for specifying the system components themselves (by CSP-OZ classes), UML-RT diagrams provide the architecture description. Thus the usual architecture specification in terms of the CSP operators parallel composition, renaming and hiding is replaced by a graphical description. To preserve the formal semantics of CSP-OZ specifications, we develop a translation from UML-RT structure diagrams to CSP. Besides achieving a more easily accessible, graphical architecture modelling for CSP-OZ, we thus also give a semantics to UML-RT structure diagrams.

[BO01]

M. Broy and E.-R. Olderog. Trace-Oriented Models of Concurrency. In J.A. Bergstra, A. Ponse, and S.A. Scott, editors, Handbook of Process Algebra, pages 101-195. Elsevier Science B.V., 2001.
[ bib ]

This chapter provides an in-depth presentation of trace-oriented models of concurrent processes. We begin by introducing and investigating finite traces as a simple abstraction of the transition behaviour of automata. Using finite traces safety properties of processes can be modelled. Later infinite traces or streams together with stream processing functions are studied. Using infinite traces more advanced phenomena like fairness and liveness properties can be modelled. We discuss and relate operational, denotational, algebraic and logical approaches to trace-oriented models and explain methods for the specification and verification of process behaviour based on these models.

[DT01]

H. Dierks and J. Tapken. Moby/PLC: Eine graphische Entwicklungsumgebung für SPS-Programme. at-Automatisierungstechnik, 1:38-44, 2001.
[ bib ]