Publications 2004-2006

 

2 Publications 2004-2006 (with Abstracts)

[QS06]

J.-D. Quesel and A. Schäfer. Spatio-temporal model checking for mobile real-time systems. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, LNCS, pages 347-361, 2006.
[ bib ]

This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. To this end, we provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study ``generalised railroad crossing'' (GRC) enriched by requirements inexpressible in non-spatial formalisms.

[BMW06]

I. Brückner, B. Metzler, and H. Wehrheim. Optimizing slicing of formal specifications by deductive verification. Nordic Journal of Computing, 13(1-2):22-45, August 2006.
[ bib | .pdf ]

Slicing is a technique for extracting parts of programs or specifications with respect to certain criteria of interest. The extraction is carried out in such a way that properties as described by the slicing criterion are preserved, i.e., they hold in the complete program if and only if they hold in the sliced program. During verification, slicing is often employed to reduce the state space of specifications to a size tractable by a model checker.

The computation of specification slices relies on the construction of dependence graphs, reflecting (at least) control and data dependencies in specifications. The more dependencies the graph has, the less removal of parts is possible. In this paper we present a technique for optimizing the construction of the dependence graph by using deductive verification techniques. More precisely, we propose a technique for showing that certain control dependencies in the graph can be eliminated. The technique employs small deductive proofs of the enabledness of certain transitions. Thereby we obtain dependence graphs with less control dependencies and as a consequence smaller specification slices which are an easier target for model checking.

[MFR06]

Roland Meyer, Johannes Faber, and Andrey Rybalchenko. Model checking duration calculus: A practical approach. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 332-346, 2006. This publication is available at SpringerLink.
[ bib | http ]

Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and real-time aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS).

[Mey06a]

R. Meyer. Model checking the pi-calculus. In Proceedings of the International Research Training Groups Workshop, volume 3 of Trustworthy Software Systems, page 15. GITO, 2006.
[ bib ]

[FM06]

Johannes Faber and Roland Meyer. Model checking data-dependent real-time properties of the european train control system. In Formal Methods in Computer Aided Design, 2006. FMCAD '06, pages 76-77. IEEE Computer Society Press, November 2006. This publication is available free of charge at IEEE Digital Library.
[ bib ]

The behavior of embedded hardware and software systems is determined by at least three dimensions: control flow, data aspects, and real-time requirements. To specify the different dimensions of a system with the best-suited techniques, the formal language CSP-OZ-DC integrates Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC) into a declarative formalism equipped with a unified and compositional semantics. In this paper, we provide evidence that CSP-OZ-DC is a convenient language for modeling systems of industrial relevance. To this end, we examine the emergency message handling in the European Train Control System (ETCS) as a case study with uninterpreted constants and infinite data domains. We automatically verify that our model ensures real-time safety properties, which crucially depend on the system?s data handling.

[SS06]

Tim Strazny and Christian Stehno. Ein Simulator für mehrfach erweiterte höhere Petrinetze. In Matthias Becker and Helena Szczerbicka, editors, 19. Symposium Simulationstechnik (ASIM 2006), pages 171-176. SCS Publishing House e.V., September 2006.
[ bib ]

[OS06]

E.-R. Olderog and B. Steffen. Formale Semantik und Programmverifikation. In P. Rechenberg and G. Pomberger, editors, Informatik-Handbuch, 4. Auflage, pages 145-166. Hanser Verlag, 2006.
[ bib ]

[SBO06]

P. E. Sevinç, D. Basin, and E.-R. Olderog. Controlling access to documents: A formal access control model. In Günter Müller, editor, ETRICS 2006, volume 3995 of LNCS, pages 352-367. Springer-Verlag, June 2006.
[ bib ]

Current access-control systems for documents suffer from one or more of the following limitations: they are coarse-grained, limited to XML documents, ot unable to maintain control over copies of documents once they are released by the system. We present a formal model of a system that overcomes all of these restrictions. It is very fine-grained, supporst a general class of documents, and provides a foundation for usage control.

[BP06]

Bernhard Beckert and André Platzer. Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In U. Furbach and N. Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS, pages 266-280. Springer-Verlag, 2006. (c) Springer-Verlag.
[ bib | .pdf ]

We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, non-rigid functions allow to embed notions of object-orientation in dynamic logic, thereby forming a basis for verification of object-oriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essential aspects of the complex verification system KeY and, hence, constitutes a foundation for object-oriented verification with the principles of reasoning that underly the successful KeY case studies.

Keywords: dynamic logic, sequent calculus, program logic, software verification, logical foundations of programming languages, object-orientation

[DHO06]

W. Damm, H. Hungar, and E.-R. Olderog. Verification of cooperating traffic agents. International Journal of Control, 79(5):395-421, May 2006.
[ bib ]

This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS, the Traffic Alert and Collision Avoidance System), train applications (such as ETCS, the European Train Control System), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by off-line analysis of the worst-case behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. A companion paper will show how such local proof obligations can be discharged automatically.

[Mey06b]

R. Meyer. Model checking using testing. In W. Hasselbring and S. Giesecke, editors, Dependability Engineering, volume 2 of Trustworthy Software Systems, pages 147-171. GITO, 2006.
[ bib ]

[BM05]

I. Brückner and B. Metzler. Deductive Verification for Improving Slicing of Integrated Formal Specifications. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 39-41. University of Copenhagen, Denmark, October 2005.
[ bib | .pdf ]

[Fab05]

Johannes Faber. Verifying real-time aspects of the European Train Control System. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 67-70. University of Copenhagen, Denmark, October 2005.
[ bib | .pdf ]

[M05]

M. Möller. Mapping formal specifications to java contracts. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 100-102. University of Copenhagen, Denmark, October 2005.
[ bib | .pdf ]

[Die05]

H. Dierks. Finding Optimal Plans for Domains with Continuous Effects with UPPAAL CORA. In Proceedings of the ICAPS'05 Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems, June 2005.
[ bib ]

[BS05]

R. Boute and A. Schäfer. The timer cascade: Functional modelling and real time calculi. In D.V. Hung and M. Wirsing, editors, Theoretical Aspects of Computing, ICTAC 2005, volume 3722 of LNCS, pages 242 - 256. Springer, 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

Case studies can significantly contribute towards improving the understanding of formalisms and thereby to their applicability in practice. One such case, namely a cascade of the familiar 24-hour timers (in suitably generalized form) provides interesting gedanken experiments and illustrations for presenting, illustrating and comparing various formalisms for modelling real-time behaviour of systems. The timer cascade is first modelled in a general-purpose functional formalism (Funmath) and various properties are derived, including an interesting algebraic monoid structure of timer programs. Then it is described and analyzed in duration calculus, thereby highlighting, similarities and differences in the approach to modelling and reasoning, and also the link between the formalisms. Future work consists in using this case as a running example for exploring the same issues for other formalisms intended for real time and hybrid systems. The underlying idea is that other authors join this effort and contribute towards extending it, finally arriving at a broad comparative survey of such formalisms.

[BW05b]

Ingo Brückner and Heike Wehrheim. Slicing an Integrated Formal Method for Verification. In Kung-Kiu Lau and Richard Banach, editors, ICFEM 2005: Seventh International Conference on Formal Engineering Methods, volume 3785 of Lecture Notes in Computer Science, pages 360-374. Springer, November 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

Model checking specifications with complex data and behaviour descriptions often fails due to the large state space to be processed. In this paper we propose a technique for reducing such specifications (with respect to certain properties under interest) before verification. The method is an adaption of the slicing technique from program analysis to the area of integrated formal notations and temporal logic properties. It solely operates on the syntactic structure of the specification which is usually significantly smaller than its state space. We show how to build a reduced specification via the construction of a so called program dependence graph, and prove correctness of the technique with respect to a projection relationship between full and reduced specification. The reduction thus preserves all properties formulated in temporal logics which are invariant under stuttering, as for instance LTL_-X.

[HM05]

Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, FM 2005, volume 3582 of LNCS, pages 465-480. Springer, 2005.
[ bib | .pdf ]

We present a new model-checking technique for CSP-OZ-DC, a combination of CSP, Object-Z and Duration Calculus, that allows reasoning about systems exhibiting communication, data and real-time aspects. As intermediate layer we will use a new kind of timed automata that preserve events and data variables of the specification. These automata have a simple operational semantics that is amenable to verification by a constraint-based abstraction-refinement model checker. By means of a case study, a simple elevator parameterised by the number of floors, we show that this approach admits model-checking parameterised and infinite state real-time systems.

[EFM⁺05]

C. Eichner, H. Fleischhack, R. Meyer, U. Schrimpf, and C. Stehno. Compositional semantics for uml 2.0 sequence diagrams using petri nets. In SDL 2005: Model Driven, volume 3530 of LNCS, pages 133-148. Springer-Verlag, 2005.
[ bib ]

[Sch05a]

A. Schäfer. Axiomatisation and Decidability of Multi-Dimensional Duration Calculus. In J. Chomicki and D. Toman, editors, Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, TIME 2005, pages 122-130. IEEE Computer Society, June 2005. This publication is available at IEEE Digital Library.
[ bib | .pdf ]

We investigate properties of a spatio-temporal logic based on an n-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in n-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use.

[OW05]

E.-R. Olderog and H. Wehrheim. Specification and (property) inheritance in CSP-OZ. Science of Computer Programming, 55:227-257, 2005.
[ 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 failure divergence model of CSP. In this paper we explain CSP-OZ and investigate the notion of inheritance. Furthermore, we study the issue of property inheritance among classes. We prove in a uniform way that behavioural subtyping relations between classes introduced in [Weh02] guarantee the inheritance of safety and ``liveness'' properties. Key words: CSP, Object-Z, failures divergence semantics, inheritance, safety and ``liveness'' properties, model-checking, FDR

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.

[Brü05]

I. Brückner. Slicing CSP-OZ Specifications for Verification. Poster Session, 4th International Conference of B and Z Users (ZB '05), April 2005.
[ bib ]

[BW05a]

I. Brückner and H. Wehrheim. Slicing Object-Z Specifications for Verification. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, volume 3455 of LNCS, pages 414-433. Springer, April 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

Slicing is the activity of reducing a program or a specification with respect to a given condition (the slicing criterion) such that the condition holds on the full program if and only if it holds on the reduced program. Originating from program analysis the entity to be sliced is usually a program and the slicing criterion a value of a variable at a certain program point. In this paper we present an approach to slicing Object-Z specifications with temporal logic formulae as slicing criteria and show the correctness of our approach. The underlying motivation is the goal to substantially reduce the size of the specification and subsequently facilitate verification of temporal logic properties.

[Sch05b]

A. Schäfer. A calculus for shapes in time and space. In Z. Liu and K. Araki, editors, Theoretical Aspects of Computing, ICTAC 2004, volume 3407 of LNCS, pages 463-478. Springer, 2005. This publication is available at SpringerLink.
[ bib | .pdf ]

We present a spatial and temporal logic based on Duration Calculus for the specification and verification of mobile real-time systems. We demonstrate the use of the formalism and apply it to a case study. We extend a pure Duration Calculus specification for the controller by spatial assumptions to reason about spatial system properties. We prove that the formalism is undecidable in general for discrete and continuous domains and present a decidable fragment.

[Brü04]

I. Brückner. Slicing CSP-OZ Specifications. In P. Pettersson and W. Yi, editors, Proceedings of the 16th Nordic Workshop on Programming Theory, number 2004-041 in Technical Reports of the Department of Information Technology, pages 71-73. Uppsala University, Sweden, October 2004.
[ bib | .pdf ]

[Die04]

H. Dierks. Heuristic guided model-checking of real-time systems. In P. Pettersson and Wang Yi, editors, Proceedings of the 16th Nordic Workshop on Programming Theory, number 2004-041 in Technical Reports of the Department of Information Technology, pages 14-16. Uppsala University, Sweden, October 2004.
[ bib ]

[BHB⁺04]

M. Bretschneider, H.-J. Holberg, E. Böde, I. Brückner, T. Peikenkamp, and H. Spenke. Model-based Safety Analysis of a Flap Control System. In T. Fossnes and M. Galinier, editors, Proceedings of the 14th Annual International INCOSE Symposium 2004, Toulouse, June 2004.
[ bib | .pdf ]

Fault tree analysis is a widely adopted technique to systematically analyze causes for a given failure of a complex system. Traditionally, a fault tree is constructed top-down based on knowledge about the structure of the system and the interaction of subsystems. With the increasing system complexity and the accompanying introduction of model-based development techniques in the industrial process, a substantial amount of this knowledge is laid down in the system models. The main focus of the presented techniques and tools is to automatically exploit this knowledge by extracting a fault tree suitable for FaulTree+ directly from a given design modeled in Statemate. The resulting fault tree is complete wrt. the specified failure, i.e. the analysis considers every possible causal failure combination which is guaranteed by applying model checking techniques. Using an aircraft Flap control system this paper shows how to smoothly integrate the technique into an existing model-based process.

[DHO04]

W. Damm, H. Hungar, and E.-R. Olderog. On the verification of cooperating traffic agents. In F.S. de Boer, M.M. Bonsangue, S. Graf, and W.-P. de Roever, editors, FMCO 2003: Formal Methods for Components and Objects, volume 3188 of LNCS, pages 77-110, 2004.
[ bib ]

This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented veri cation methodology is equally applicable for avionics applications (such as TCAS), train applications (such as ETCS), or automotive applications (such as platooning). We present a veri cation rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by o -line analysis of the worst-case behavior of the involved tra c agents, or by purely local proofs, involving only a single tra c agent. In a companion paper we will show, how such local proof obligations can be discharged automatically.

[Weh04]

H. Wehrheim. Preserving properties under change. In F.S. de Boer, M.M. Bonsangue, S. Graf, and W.-P. de Roever, editors, FMCO 2003: Formal Methods for Components and Objects, volume 3188 of LNCS, pages 330-343, 2004.
[ bib ]

[FW04]

C. Fischer and H. Wehrheim. Failure-Divergence Semantics as a Formal Basis for an Object-Oriented Integrated Formal Method. In G. Paun, G. Rozenberg, and A. Salomaa, editors, Current Trends in Theoretical Computer Science: The Challenge of the New Century, Vol 2: Formal Models and Semantics. World Scientific, 2004.
[ bib ]

[BBB⁺04]

R. Buschermöhle, M. Brörkens, I. Brückner, W. Damm, W. Hasselbring, B. Josko, C. Schulte, and T. Wolf. Model Checking - Grundlagen und Praxiserfahrungen. Informatik Spektrum, 27(2):146-158, April 2004.
[ bib | .pdf ]

The correct functioning of hard- and software components is often a crucial factor in computer-based system engineering. Particularly, this is the case in the area of 'safety critical' systems, where a system failure can endanger human life. But also in less critical areas the correctness of provided functionality becomes more and more important. Furthermore the complexity of system functionality increases steadily. Therefore manual test and simulation methods can detect many errors only with inaccaptable high effort concerning time and resources. Starting from this background, this article presents the basics of 'model checking', an automatic and complete verification method. Based on this introduction, experience gained with the application of model checking tools in industrial contexts is presented and discussed.

[MORW04]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Linking CSP-OZ with UML and Java: A Case Study. In E. Boiten, J. Derrick, and G. Smith, editors, Integrated Formal Methods, number 2999 in Lecture Notes in Computer Science, pages 267-286. Springer-Verlag, March 2004.
[ bib | .pdf ]

We describe how CSP-OZ, an integrated formal method combining the process algebra CSP with the specification language Object-Z, can be linked to standard software engineering languages, viz. UML and Java. Our aim is to generate a significant part of the CSP-OZ specification from an initially developed UML model using a UML profile for CSP-OZ, and afterwards transform the formal specification into assertions written in the Java Modelling Language JML complemented by CSP_jassda. The intermediate CSP-OZ specification serves to verify correctness of the UML model, and the assertions control at runtime the adherence of a Java implementation to these formal requirements. We explain this approach using the case study of a ``holonic manufacturing system'' in which coordination of transportation and processing is distributed among stores, machine tools and agents without central control.