Publications of year 2003

Articles in conference or workshop proceedings

  1. Dirk Beyer and Claus Lewerentz. CrocoPat: Efficient Pattern Analysis in Object-Oriented Programs. In Proceedings of the 11th IEEE International Workshop on Program Comprehension (IWPC 2003, Portland, OR, May 10-11), pages 294-295, 2003. IEEE Computer Society Press, Los Alamitos (CA). [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    Automatic pattern-based 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 real-world 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 object-oriented programs (1'000 to 10'000~classes) in acceptable time.
    Annotation:
    IWPC 2003, Portland, OR, May 10-11
    Introduction of a BDD-based 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 Object-Oriented Programs},
    booktitle = {Proceedings of the 11th IEEE International Workshop on Program Comprehension (IWPC~2003, Portland, OR, May 10-11)},
    pages = {294-295},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    year = {2003},
    isbn = {0-7695-1883-4},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2003-IWPC.CrocoPat_Efficient_Pattern_Analysis_in_Object-Oriented_Programs.pdf},
    url = {http://www.sosy-lab.org/~dbeyer/CrocoPat/},
    abstract = { Automatic pattern-based 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 real-world 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 object-oriented programs (1'000 to 10'000~classes) in acceptable time. }, annote = {IWPC 2003, Portland, OR, May 10-11
    Introduction of a BDD-based tool for pattern analysis and a short overview of the main features of CrocoPat. }, }

  2. Dirk Beyer, Claus Lewerentz, and Andreas Noack. Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. In W. A. Hunt and F. Somenzi, editors, Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003, Boulder, CO, July 8-12), LNCS 2725, pages 122-125, 2003. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    This paper gives a short overview of a model checking tool for real-time 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 BDD-based version of Kronos.
    Annotation:
    CAV 2003, Boulder, CO, July 8-12,
    Warren A. Hunt Jr., Fabio Somenzi, editors.
    © 2006 Springer-Verlag
    Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122
    A description of the BDD-based tool's main features.

    @InProceedings{CAV03,
    author = {Dirk Beyer and Claus Lewerentz and Andreas Noack},
    title = {Rabbit: A Tool for {BDD}-Based Verification of Real-Time Systems},
    booktitle = {Proceedings of the 15th International Conference on Computer Aided Verification (CAV~2003, Boulder, CO, July 8-12)},
    editor = {W.~A.~Hunt and F.~Somenzi},
    series = {LNCS~2725},
    pages = {122-125},
    publisher = {Springer-Verlag, Heidelberg},
    year = {2003},
    isbn = {3-540-40524-0},
    keyword = {Formal Verification of Real-Time Systems},
    pdf = {https://www.sosy-lab.org/research/pub/2003-CAV.Rabbit_A_Tool_for_BDD-Based_Verification_of_Real-Time_Systems.pdf},
    url = {},
    abstract = { This paper gives a short overview of a model checking tool for real-time 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 BDD-based version of Kronos. },
    annote = { CAV 2003, Boulder, CO, July 8-12,
    Warren A. Hunt Jr., Fabio Somenzi, editors.
    © 2006 Springer-Verlag
    Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122
    A description of the BDD-based tool's main features. }, }

  3. Dirk Beyer and Andreas Noack. Can Decision Diagrams Overcome State Space Explosion in Real-Time 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 193-208, 2003. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time 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 non-trivial state space explosion. Secondly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-size CDDs if they use better variable orders, as the BDD-based 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.
    Annotation:
    FORTE 2003, Berlin, September 29 - October 2
    Hartmut König, Monika Heiner, Adam Wolisz, editors.
    © 2006 Springer-Verlag
    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 Real-Time 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 = {193-208},
    publisher = {Springer-Verlag, Heidelberg},
    year = {2003},
    isbn = {3-540-20175-0},
    keyword = {Formal Verification of Real-Time Systems},
    pdf = {https://www.sosy-lab.org/research/pub/2003-FORTE.Can_Decision_Diagrams_Overcome_State_Space_Explosion_in_Real-Time_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 non-trivial state space explosion. Secondly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-size CDDs if they use better variable orders, as the BDD-based 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 Springer-Verlag
    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. }, }

  4. 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 13-16), pages 216-225, 2003. IEEE Computer Society Press, Los Alamitos (CA). [ Info ] [ PDF ] 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 as-built and the as-designed 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 well-known as a compact representation of large relations in computer-aided verification. CrocoPat is general, because it manipulates not only graphs (i.e. binary relations), but n-ary relations.
    Annotation:
    WCRE 2003, Victoria, BC, November 13-16
    CrocoPat's concepts, an introduction to the BDD-based 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 13-16)},
    pages = {216-225},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    year = {2003},
    isbn = {0-7695-2027-8},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2003-WCRE.Simple_and_Efficient_Relational_Querying_of_Software_Structures.pdf},
    url = {http://www.sosy-lab.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 as-built and the as-designed 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 well-known as a compact representation of large relations in computer-aided verification. CrocoPat is general, because it manipulates not only graphs (i.e. binary relations), but n-ary relations. },
    annote = { WCRE 2003, Victoria, BC, November 13-16 
    CrocoPat's concepts, an introduction to the BDD-based implementation, software analysis applications, and performance measurements.
    Online: http://dx.doi.org/10.1109/WCRE.2003.1287252
    }, }

Internal reports

  1. Dirk Beyer and Claus Lewerentz. CrocoPat: A Tool for Efficient Pattern Recognition in Large Object-Oriented Programs. Technical report I-04/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003. [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Annotation:
    See WCRE03 [27] for proceedings version.

    @TechReport{TR04-BTU03,
    author = {Dirk Beyer and Claus Lewerentz},
    title = {{CrocoPat}: A Tool for Efficient Pattern Recognition in Large Object-Oriented Programs},
    institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus},
    month = {January},
    year = {2003},
    number = {I-04/2003},
    pdf = {https://www.sosy-lab.org/research/pub/2003-BTU-TR04.CrocoPat_A_Tool_for_Efficient_Pattern_Recognition.in_Large_Object-Oriented_Programs.pdf},
    keyword = {Structural Analysis and Comprehension},
    annote = {See WCRE03 [27] for proceedings version.},
    
    }
    

  2. Dirk Beyer and Andreas Noack. A Comparative Study of Decision Diagrams for Real-Time Verification. Technical report I-03/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See FORTE03 [26] for proceedings version.

    @TechReport{TR03-BTU03,
    author = {Dirk Beyer and Andreas Noack},
    title = {A Comparative Study of Decision Diagrams for Real-Time Verification},
    institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus},
    month = {January},
    year = {2003},
    number = {I-03/2003},
    keyword = {Formal Verification of Real-Time 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 18 13:27:46 2017


This document was translated from BibTEX by bibtex2html