Dr. Ingo Brückner
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@INPROCEEDINGS{ib07ifm,
AUTHOR = {I. Br{\"u}ckner},
TITLE = {{Slicing Concurrent Real-Time System Specifications for
Verification}},
BOOKTITLE = {Integrated Formal Methods},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4591},
PUBLISHER = {Springer-Verlag},
ISSN = {0302-9743},
ISBN = {978-3-540-73209-9},
EDITOR = {J. Davies and J. Gibbons},
PAGES = {54--74},
MONTH = JUL,
YEAR = {2007},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07ifm.pdf}
}
@INPROCEEDINGS{BDFW07,
AUTHOR = {I. Br\"uckner and K. Dr\"ager and B. Finkbeiner and H. Wehrheim},
TITLE = {{Slicing Abstractions}},
BOOKTITLE = {FSEN 2007: IPM International Symposium on Fundamentals of
Software Engineering},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4767},
PUBLISHER = {Springer},
ISSN = {},
ISBN = {978-3-540-75697-2},
EDITOR = {F. Arbab and M. Sirjani},
PAGES = {17--32},
MONTH = {April},
YEAR = {2007},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07fsen.pdf}
}
@ARTICLE{BMW06,
AUTHOR = {I. Br\"uckner and B. Metzler and H. Wehrheim},
TITLE = {Optimizing Slicing of Formal Specifications by Deductive
Verification},
JOURNAL = {Nordic Journal of Computing},
YEAR = {2006},
VOLUME = {13},
NUMBER = {1--2},
MONTH = {August},
PAGES = {22--45},
ABSTRACT = {
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 {\em 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.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib06njc.pdf}
}
@INPROCEEDINGS{ibnwpt05,
AUTHOR = {I. Br{\"u}ckner and B. Metzler},
TITLE = {{Deductive Verification for Improving Slicing of Integrated
Formal
Specifications}},
BOOKTITLE = {Proceedings of the 17th Nordic Workshop on Programming Theory},
PUBLISHER = {University of Copenhagen, Denmark},
PAGES = {39--41},
YEAR = {2005},
MONTH = {October},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05-nwpt.pdf}
}
@INPROCEEDINGS{BW05b,
AUTHOR = {Ingo Br\"uckner and Heike Wehrheim},
TITLE = {{Slicing an Integrated Formal Method for Verification}},
BOOKTITLE = {ICFEM 2005: Seventh International Conference on Formal
Engineering Methods},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3785},
PUBLISHER = {Springer},
ISSN = {0302-9743},
ISBN = {3-540-29797-9},
EDITOR = {Kung-Kiu Lau and Richard Banach},
PAGES = {360--374},
MONTH = {November},
YEAR = {2005},
ABSTRACT = {
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 {\em reducing}
such specifications (with respect to certain properties under
interest) before verification. The method is an adaption of the
{\em 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}$.
},
NOTE = { This publication is available at
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3785&spage=360}
{SpringerLink}
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05icfem.pdf}
}
@TECHREPORT{BW05bTR,
AUTHOR = {I. Br\"uckner and H. Wehrheim},
TITLE = {{Slicing CSP-OZ Specifications for Verification}},
NUMBER = {7},
INSTITUTION = {{SFB/TR 14 AVACS}},
ADDRESS = {http://www.avacs.org/},
URL = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_007.pdf},
YEAR = {2005},
}
@MISC{ib05zb,
AUTHOR = {I. Br{\"u}ckner},
TITLE = {{Slicing CSP-OZ Specifications for Verification}},
HOWPUBLISHED = {Poster Session, 4th International Conference
of B and Z Users (ZB '05)},
MONTH = {April},
YEAR = {2005},
}
@INPROCEEDINGS{BW05a,
AUTHOR = {I. Br\"uckner and H. Wehrheim},
TITLE = {{Slicing Object-Z Specifications for Verification}},
BOOKTITLE = {ZB 2005: Formal Specification and Development in Z and B},
SERIES = {LNCS},
VOLUME = {3455},
PUBLISHER = {Springer},
ISSN = {0302-9743},
ISBN = {3-540-25559-1},
EDITOR = {H. Treharne and S. King and M. Henson and S. Schneider},
PAGES = {414--433},
MONTH = {April},
YEAR = {2005},
ABSTRACT = {
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.
},
NOTE = {This publication is available at
\url{
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volum
e=3455&spage=414}
{SpringerLink}
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib05zb.pdf}
}
@TECHREPORT{BW05aTR,
AUTHOR = {I. Br\"uckner and H. Wehrheim},
TITLE = {{Slicing Object-Z Specifications for Verification}},
NUMBER = {3},
INSTITUTION = {{SFB/TR 14 AVACS}},
ADDRESS = {http://www.avacs.org/},
URL = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_003.pdf},
YEAR = {2005},
}
@INPROCEEDINGS{nwpt04,
AUTHOR = {I. Br{\"u}ckner},
TITLE = {{Slicing CSP-OZ Specifications}},
EDITOR = {P. Pettersson and W. Yi},
BOOKTITLE = {Proceedings of the 16th Nordic Workshop on Programming Theory},
SERIES = {Technical Reports of the Department of Information Technology},
NUMBER = {2004-041},
PUBLISHER = {Uppsala University, Sweden},
ISSN = {1404-3203},
PAGES = {71--73},
YEAR = {2004},
MONTH = {October},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib04nwpt.pdf}
}
@INPROCEEDINGS{incose04,
AUTHOR = {M. Bretschneider and H.-J. Holberg and E. B\"ode and I.
Br\"uckner
and T. Peikenkamp and H. Spenke},
TITLE = {{Model-based Safety Analysis of a Flap Control System}},
BOOKTITLE = {Proceedings of the 14th Annual International INCOSE Symposium
2004, Toulouse},
EDITOR = {T. Fossnes and M. Galinier},
MONTH = {June},
YEAR = {2004},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib04ft.pdf}
}
@ARTICLE{mcp04,
AUTHOR = {R. Buscherm\"ohle and M. Br\"orkens and I. Br\"uckner and
W. Damm and W. Hasselbring and B. Josko and C. Schulte and T. Wolf},
TITLE = {{Model Checking -- Grundlagen und Praxiserfahrungen}},
JOURNAL = {Informatik Spektrum},
EDITOR = {A. Bode},
ISSN = {0170-6012},
PUBLISHER = {Springer Verlag},
VOLUME = {27},
NUMBER = {2},
PAGES = {146--158},
MONTH = {April},
YEAR = {2004},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib04mc.pdf}
}
@ARTICLE{mcpees03,
AUTHOR = {C. Schulte and M. Br\"orkens and I. Br\"uckner and
R. Buscherm\"ohle and T. Wolf},
TITLE = {{Sicherheit f\"ur sicherheitskritische Systeme}},
JOURNAL = {Electronic Embedded Systeme},
ISSN = {0943-4941},
PUBLISHER = {AWi Verlag},
MONTH = {September},
PAGES = {19-21},
YEAR = {2003},
ABSTRACT = {
Mikroprozessoren werden immer h\"aufiger auch in technischen
Ger\"aten und vielerlei allt\"aglichen Konsumg\"utern eingesetzt.
Letzere werden auch als eingebettete Systeme bezeichnet, das
hei\ss{}t in umgebende technische Systeme wechselseitig
integrierte Computersysteme. Die Entwicklung solcher eingebetteter
Systeme wird unter anderem aufgrund immer h\"oherer Anforderungen
an die Funktionalit\"at 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\"andige
Korrektheitsnachweise gefordert. Ein aussichtsreicher Kandidat in
diesem Kontext ist das Model-Checking.
},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib03.pdf}
}
