Software and Computational Systems Lab

Publications of year 2003

1. Dirk Beyer. Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata (Zusammenfassung). Softwaretechnik-Trends, 23(2):4, May 2003. Gesellschaft für Informatik, Berlin.
   BibTeX Entry

   @article{SW-Trends03, author = {Dirk Beyer}, title = {Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata (Zusammenfassung)}, journal = {Softwaretechnik-Trends}, volume = {23}, number = {2}, pages = {4}, year = {2003}, publisher = {Gesellschaft f{\"u}r Informatik, Berlin}, annote = {Summary of dissertation}, doinone = {DOI not available}, issn = {0720-8928}, month = {May}, }
   Additional Infos

   Summary of dissertation

2. 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). doi:10.1109/WCRE.2003.1287252 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF Supplement
   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.
   BibTeX Entry

   @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}, year = {2003}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {0-7695-2027-8}, doi = {10.1109/WCRE.2003.1287252}, url = {http://www.sosy-lab.org/~dbeyer/CrocoPat/}, pdf = {https://www.sosy-lab.org/research/pub/2003-WCRE.Simple_and_Efficient_Relational_Querying_of_Software_Structures.pdf}, 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.}, keyword = {Structural Analysis and Comprehension}, annote = {CrocoPat's concepts, an introduction to the BDD-based implementation, software analysis applications, and performance measurements.<BR>}, }
   Additional Infos

   CrocoPat's concepts, an introduction to the BDD-based implementation, software analysis applications, and performance measurements.
   
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. doi:10.1007/978-3-540-39979-7_13 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF
   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.
   BibTeX Entry

   @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}, pages = {193-208}, year = {2003}, series = {LNCS~2767}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-20175-0}, doi = {10.1007/978-3-540-39979-7_13}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2003-FORTE.Can_Decision_Diagrams_Overcome_State_Space_Explosion_in_Real-Time_Verification.pdf}, 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {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.}, }
   Additional Infos

   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, 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. doi:10.1007/978-3-540-45069-6_13 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF
   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.
   BibTeX Entry

   @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}, pages = {122-125}, year = {2003}, series = {LNCS~2725}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-40524-0}, doi = {10.1007/978-3-540-45069-6_13}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2003-CAV.Rabbit_A_Tool_for_BDD-Based_Verification_of_Real-Time_Systems.pdf}, 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {Online: <a href="http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122"> http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122</a> <BR> A description of the BDD-based tool's main features.}, }
   Additional Infos

   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.
5. 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). doi:10.1109/WPC.2003.1199220 Keyword(s): Structural Analysis and Comprehension Publisher's Version PDF Supplement
   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.
   BibTeX Entry

   @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}, year = {2003}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {0-7695-1883-4}, doi = {10.1109/WPC.2003.1199220}, url = {http://www.sosy-lab.org/~dbeyer/CrocoPat/}, pdf = {https://www.sosy-lab.org/research/pub/2003-IWPC.CrocoPat_Efficient_Pattern_Analysis_in_Object-Oriented_Programs.pdf}, 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. <BR> 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.}, keyword = {Structural Analysis and Comprehension}, annote = {Introduction of a BDD-based tool for pattern analysis and a short overview of the main features of CrocoPat.}, }
   Additional Infos

   Introduction of a BDD-based tool for pattern analysis and a short overview of the main features of CrocoPat.

6. 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. Keyword(s): Structural Analysis and Comprehension PDF
   BibTeX Entry

   @techreport{TR04-BTU03, author = {Dirk Beyer and Claus Lewerentz}, title = {{CrocoPat}: A Tool for Efficient Pattern Recognition in Large Object-Oriented Programs}, number = {I-04/2003}, year = {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.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {January}, }
   Additional Infos

   See WCRE03 [27] for proceedings version.
7. 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
   BibTeX Entry

   @techreport{TR03-BTU03, author = {Dirk Beyer and Andreas Noack}, title = {A Comparative Study of Decision Diagrams for Real-Time Verification}, number = {I-03/2003}, year = {2003}, keyword = {Formal Verification of Real-Time Systems}, annote = {See FORTE03 [26] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {January}, }
   Additional Infos

   See FORTE03 [26] for proceedings version.

8. CrocoPat: Relational Programming (for Software-Structure Analysis). 2003. Keyword(s): Software Development Project, Structural Analysis and Comprehension Supplement
   BibTeX Entry

   @misc{CrocoPat, title = {{{\sc CrocoPat}}: Relational Programming (for Software-Structure Analysis)}, year = {2003}, url = {http://www.sosy-lab.org/~dbeyer/CrocoPat/}, keyword = {Software Development Project,Structural Analysis and Comprehension}, role = {Principal designer and implementer}, }