Dr. Ingo Brückner

 

1 Publications (with abstracts)

[Brü07]

I. Brückner. Slicing Concurrent Real-Time System Specifications for Verification. In J. Davies and J. Gibbons, editors, Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 54-74. Springer-Verlag, July 2007.
[ bib | .pdf ]

The high-level specification language CSP-OZ-DC has been shown to be well-suited for modelling and analysing industrially relevant concurrent real-time systems. It allows to model each of the most important functional aspects such as control flow, data, and real-time requirements in adequate notations, maintaining a common semantical foundation for subsequent verification. Slicing on the other hand has become an established technique to complement the fight against state space explosion during verification which inherently accompanies increasing system complexity. In this paper, we exploit the special structure of CSP-OZ-DC specifications by extending the dependence graph-which usually serves as a basis for slicing-with several new types of dependencies, including timing dependencies derived from the specification's DC part. Based on this we show how to compute a specification slice and prove correctness of our approach.

[BDFW07]

I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim. Slicing Abstractions. In F. Arbab and M. Sirjani, editors, FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering, volume 4767 of Lecture Notes in Computer Science, pages 17-32. Springer, April 2007.
[ bib | .pdf ]

Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct.

[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.

[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 ]

[BW05d]

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.

[BW05a]

I. Brückner and H. Wehrheim. Slicing CSP-OZ Specifications for Verification. Technical Report 7, SFB/TR 14 AVACS, http://www.avacs.org/, 2005.
[ bib | .pdf ]

[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 ]

[BW05b]

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.

[BW05c]

I. Brückner and H. Wehrheim. Slicing Object-Z Specifications for Verification. Technical Report 3, SFB/TR 14 AVACS, http://www.avacs.org/, 2005.
[ bib | .pdf ]

[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 ]

[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.

[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.

[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.