Publications of year 2003
Articles in journal or book chapters

Dirk Beyer.
Formale Verifikation von RealzeitSystemen mittels Cottbus Timed Automata (Zusammenfassung).
SoftwaretechnikTrends, 23(2):4, May 2003.
Summary of dissertation@Article{SWTrends03, author = {Dirk Beyer}, title = {Formale Verifikation von RealzeitSystemen mittels Cottbus Timed Automata (Zusammenfassung)}, journal = {SoftwaretechnikTrends}, publisher = {Gesellschaft f{\"u}r Informatik, Berlin}, volume = {23}, number = {2}, pages = {4}, month = {May}, year = {2003}, issn = {07208928}, annote = {Summary of dissertation}, }
Articles in conference or workshop proceedings

Dirk Beyer and Claus Lewerentz.
CrocoPat: Efficient Pattern Analysis in ObjectOriented Programs.
In Proceedings of the 11th IEEE International Workshop on Program Comprehension (IWPC 2003, Portland, OR, May 1011), pages 294295, 2003.
IEEE Computer Society Press, Los Alamitos (CA).
[ Material ] [ Article ] Keyword(s): Structural Analysis and Comprehension.
Abstract
Automatic patternbased recognition of design weakness is a research topic since almost 10 years. Reports about experiments with existing approaches reveal two major problems: A notation for easy and flexible specification of the pattern is missing; only a restricted set of patterns is applicable because of the limitations of the specification language. Performance improvement is needed, because the computation time of existing tools is to high to be acceptable for large realworld systems.
The tool CrocoPat satisfies the following three requirements: (1) The analysis is done automatically by the tool, i.e. without user interaction. (2) The properties of a system are specified in an easy and flexible way because the patterns are described by relational expressions. On demand the user is able to define new patterns he is interested in, or to change existing patterns to solve specific problems. (3) The tool is able to analyze large objectoriented programs (1'000 to 10'000~classes) in acceptable time.IWPC 2003, Portland, OR, May 1011
Introduction of a BDDbased tool for pattern analysis and a short overview of the main features of CrocoPat.@InProceedings{IWPC03, author = {Dirk Beyer and Claus Lewerentz}, title = {{{\sc CrocoPat}}: Efficient Pattern Analysis in ObjectOriented Programs}, booktitle = {Proceedings of the 11th IEEE International Workshop on Program Comprehension (IWPC~2003, Portland, OR, May 1011)}, pages = {294295}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, year = {2003}, isbn = {0769518834}, keyword = {Structural Analysis and Comprehension}, pdf = {https://www.sosylab.org/research/pub/2003IWPC.CrocoPat_Efficient_Pattern_Analysis_in_ObjectOriented_Programs.pdf}, url = {http://www.sosylab.org/~dbeyer/CrocoPat/}, abstract = { Automatic patternbased recognition of design weakness is a research topic since almost 10 years. Reports about experiments with existing approaches reveal two major problems: A notation for easy and flexible specification of the pattern is missing; only a restricted set of patterns is applicable because of the limitations of the specification language. Performance improvement is needed, because the computation time of existing tools is to high to be acceptable for large realworld systems.
The tool CrocoPat satisfies the following three requirements: (1) The analysis is done automatically by the tool, i.e. without user interaction. (2) The properties of a system are specified in an easy and flexible way because the patterns are described by relational expressions. On demand the user is able to define new patterns he is interested in, or to change existing patterns to solve specific problems. (3) The tool is able to analyze large objectoriented programs (1'000 to 10'000~classes) in acceptable time. }, annote = {IWPC 2003, Portland, OR, May 1011
Introduction of a BDDbased tool for pattern analysis and a short overview of the main features of CrocoPat. }, } 
Dirk Beyer,
Claus Lewerentz,
and Andreas Noack.
Rabbit: A Tool for BDDBased Verification of RealTime Systems.
In W. A. Hunt and F. Somenzi, editors, Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003, Boulder, CO, July 812), LNCS 2725, pages 122125, 2003.
SpringerVerlag, Heidelberg.
[ Article ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
This paper gives a short overview of a model checking tool for realtime systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using the data structure BDD. Good variable orderings for the BDDs are computed from the modular structure of the model and an estimate of the BDD size. This leads to a significant performance improvement compared to the tool RED and the BDDbased version of Kronos.CAV 2003, Boulder, CO, July 812,
Warren A. Hunt Jr., Fabio Somenzi, editors.
© 2006 SpringerVerlag
Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volume=2725&spage=122
A description of the BDDbased tool's main features.@InProceedings{CAV03, author = {Dirk Beyer and Claus Lewerentz and Andreas Noack}, title = {Rabbit: A Tool for {BDD}Based Verification of RealTime Systems}, booktitle = {Proceedings of the 15th International Conference on Computer Aided Verification (CAV~2003, Boulder, CO, July 812)}, editor = {W.~A.~Hunt and F.~Somenzi}, series = {LNCS~2725}, pages = {122125}, publisher = {SpringerVerlag, Heidelberg}, year = {2003}, isbn = {3540405240}, keyword = {Formal Verification of RealTime Systems}, pdf = {https://www.sosylab.org/research/pub/2003CAV.Rabbit_A_Tool_for_BDDBased_Verification_of_RealTime_Systems.pdf}, url = {}, abstract = { This paper gives a short overview of a model checking tool for realtime systems. The modeling language are timed automata extended with concepts for modular modeling. The tool provides reachability analysis and refinement checking, both implemented using the data structure BDD. Good variable orderings for the BDDs are computed from the modular structure of the model and an estimate of the BDD size. This leads to a significant performance improvement compared to the tool RED and the BDDbased version of Kronos. }, annote = { CAV 2003, Boulder, CO, July 812,
Warren A. Hunt Jr., Fabio Somenzi, editors.
© 2006 SpringerVerlag
Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volume=2725&spage=122
A description of the BDDbased tool's main features. }, } 
Dirk Beyer and Andreas Noack.
Can Decision Diagrams Overcome State Space Explosion in RealTime Verification?.
In H. König, M. Heiner, and A. Wolisz, editors, Proceedings of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2003, Berlin, September 29  October 2), LNCS 2767, pages 193208, 2003.
SpringerVerlag, Heidelberg.
[ Article ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
In this paper we analyze the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Therefore we present analytical and empirical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. This is the first evidence that CDDs can grow only polynomially for models with nontrivial state space explosion. Secondly, they show that CDDbased tools, which currently use at least exponential space for two of the protocols, will only find polynomialsize CDDs if they use better variable orders, as the BDDbased tool Rabbit does. Finally, they give insight into the dependency of the BDD and CDD size on properties of the model, in particular the number of automata and the magnitude of the clock values.FORTE 2003, Berlin, September 29  October 2
Hartmut König, Monika Heiner, Adam Wolisz, editors.
© 2006 SpringerVerlag
Online: http://dx.doi.org/10.1007/11965
Analysis of the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Analytical and empirical complexity results for three communication protocols.@InProceedings{FORTE03, author = {Dirk Beyer and Andreas Noack}, title = {Can Decision Diagrams Overcome State Space Explosion in RealTime Verification?}, booktitle = {Proceedings of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE~2003, Berlin, September 29  October 2)}, editor = {H.~K{\"o}nig and M.~Heiner and A.~Wolisz}, series = {LNCS~2767}, pages = {193208}, publisher = {SpringerVerlag, Heidelberg}, year = {2003}, isbn = {3540201750}, keyword = {Formal Verification of RealTime Systems}, pdf = {https://www.sosylab.org/research/pub/2003FORTE.Can_Decision_Diagrams_Overcome_State_Space_Explosion_in_RealTime_Verification.pdf}, url = {}, abstract = { In this paper we analyze the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Therefore we present analytical and empirical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. This is the first evidence that CDDs can grow only polynomially for models with nontrivial state space explosion. Secondly, they show that CDDbased tools, which currently use at least exponential space for two of the protocols, will only find polynomialsize CDDs if they use better variable orders, as the BDDbased tool Rabbit does. Finally, they give insight into the dependency of the BDD and CDD size on properties of the model, in particular the number of automata and the magnitude of the clock values. }, annote = { FORTE 2003, Berlin, September 29  October 2
Hartmut König, Monika Heiner, Adam Wolisz, editors.
© 2006 SpringerVerlag
Online: http://dx.doi.org/10.1007/11965
Analysis of the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Analytical and empirical complexity results for three communication protocols. }, } 
Dirk Beyer,
Andreas Noack,
and Claus Lewerentz.
Simple and Efficient Relational Querying of Software Structures.
In Proceedings of the Tenth IEEE Working Conference on Reverse Engineering (WCRE 2003, Victoria, BC, November 1316), pages 216225, 2003.
IEEE Computer Society Press, Los Alamitos (CA).
[ Material ] [ Article ] Keyword(s): Structural Analysis and Comprehension.
Abstract
Many analyses of software systems can be formalized as relational queries, for example the detection of design patterns, of patterns of problematic design, of code clones, of dead code, and of differences between the asbuilt and the asdesigned architecture. This paper describes the concepts of CrocoPat, a tool for querying and manipulating relations. CrocoPat is easy to use, because of its simple query and manipulation language based on predicate calculus, and its simple file format for relations. CrocoPat is efficient, because it internally represents relations as binary decision diagrams, a data structure that is wellknown as a compact representation of large relations in computeraided verification. CrocoPat is general, because it manipulates not only graphs (i.e. binary relations), but nary relations.WCRE 2003, Victoria, BC, November 1316
CrocoPat's concepts, an introduction to the BDDbased implementation, software analysis applications, and performance measurements.
Online: http://dx.doi.org/10.1109/WCRE.2003.1287252
@InProceedings{WCRE03, author = {Dirk Beyer and Andreas Noack and Claus Lewerentz}, title = {Simple and Efficient Relational Querying of Software Structures}, booktitle = {Proceedings of the Tenth IEEE Working Conference on Reverse Engineering (WCRE~2003, Victoria, BC, November 1316)}, pages = {216225}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, year = {2003}, isbn = {0769520278}, keyword = {Structural Analysis and Comprehension}, pdf = {https://www.sosylab.org/research/pub/2003WCRE.Simple_and_Efficient_Relational_Querying_of_Software_Structures.pdf}, url = {http://www.sosylab.org/~dbeyer/CrocoPat/}, abstract = { Many analyses of software systems can be formalized as relational queries, for example the detection of design patterns, of patterns of problematic design, of code clones, of dead code, and of differences between the asbuilt and the asdesigned architecture. This paper describes the concepts of CrocoPat, a tool for querying and manipulating relations. CrocoPat is easy to use, because of its simple query and manipulation language based on predicate calculus, and its simple file format for relations. CrocoPat is efficient, because it internally represents relations as binary decision diagrams, a data structure that is wellknown as a compact representation of large relations in computeraided verification. CrocoPat is general, because it manipulates not only graphs (i.e. binary relations), but nary relations. }, annote = { WCRE 2003, Victoria, BC, November 1316
CrocoPat's concepts, an introduction to the BDDbased implementation, software analysis applications, and performance measurements.
Online: http://dx.doi.org/10.1109/WCRE.2003.1287252
}, }
Internal reports

Dirk Beyer and Claus Lewerentz.
CrocoPat: A Tool for Efficient Pattern Recognition in Large ObjectOriented Programs.
Technical report I04/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003.
[ Article ] Keyword(s): Structural Analysis and Comprehension.
See WCRE03 [27] for proceedings version.@TechReport{TR04BTU03, author = {Dirk Beyer and Claus Lewerentz}, title = {{CrocoPat}: A Tool for Efficient Pattern Recognition in Large ObjectOriented Programs}, institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {January}, year = {2003}, number = {I04/2003}, pdf = {https://www.sosylab.org/research/pub/2003BTUTR04.CrocoPat_A_Tool_for_Efficient_Pattern_Recognition.in_Large_ObjectOriented_Programs.pdf}, keyword = {Structural Analysis and Comprehension}, annote = {See WCRE03 [27] for proceedings version.}, }

Dirk Beyer and Andreas Noack.
A Comparative Study of Decision Diagrams for RealTime Verification.
Technical report I03/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003.
Keyword(s): Formal Verification of RealTime Systems.
See FORTE03 [26] for proceedings version.@TechReport{TR03BTU03, author = {Dirk Beyer and Andreas Noack}, title = {A Comparative Study of Decision Diagrams for RealTime Verification}, institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {January}, year = {2003}, number = {I03/2003}, keyword = {Formal Verification of RealTime Systems}, annote = {See FORTE03 [26] for proceedings version.}, }
Disclaimer:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
Last modified: Mon Dec 16 10:15:29 2019
This document was translated from BibT_{E}X by bibtex2html