@phdthesis{Beyer, author = {Beyer, Dirk}, title = {Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-000000258}, language = {de} } @inproceedings{BeyerHeinig, author = {Beyer, Dirk and Heinig, Andy}, title = {Different Strategies for BDD-based Reachability Analysis of Timed Automata}, series = {Proceedings of the 2nd IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2001, Washington, D.C., April 2001)}, booktitle = {Proceedings of the 2nd IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2001, Washington, D.C., April 2001)}, editor = {Rozenblit, Jerzy and Sveda, Miroslav and Rattray, Charles}, address = {Stirling}, pages = {89 -- 98}, language = {en} } @inproceedings{BeyerLewerentzSimon, author = {Beyer, Dirk and Lewerentz, Claus and Simon, Frank}, title = {Impact of Inheritance on Metrics for Size, Coupling, and Cohesion in Object Oriented Systems}, series = {New approaches in software measurement, 10th international workshop, proceedings, IWSM 2000, Berlin, Germany, October 4 - 6, 2000}, booktitle = {New approaches in software measurement, 10th international workshop, proceedings, IWSM 2000, Berlin, Germany, October 4 - 6, 2000}, editor = {Abran, Alain and Dumke, Reiner}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-41727-3}, pages = {1 -- 17}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {Efficient Verification of Timed Automata using BDDs}, series = {FMICS 2001, Formal methods for industrial critical systems, proceedings, International workshop on formal methods for industrial critical systems 6, 16 - 17 July 2001, Paris}, booktitle = {FMICS 2001, Formal methods for industrial critical systems, proceedings, International workshop on formal methods for industrial critical systems 6, 16 - 17 July 2001, Paris}, editor = {Ultes-Nitsche, Ulrich and Gnesi, Stefania}, publisher = {INRIA}, address = {Rocquencourt}, isbn = {2-7261-1187-4}, pages = {95 -- 113}, language = {en} } @inproceedings{BeyerRust, author = {Beyer, Dirk and Rust, Heinrich}, title = {Timed Automata Formal Definition and Semantics}, series = {Joint Workshop on Formal Specification of Computer-Based Systems, Washington DC, USA, April 20, 2001}, booktitle = {Joint Workshop on Formal Specification of Computer-Based Systems, Washington DC, USA, April 20, 2001}, editor = {Rattray, Charles and Sveda, Miroslav and Rozenblit, Jerzy}, publisher = {University of Stirling, Dept. of Computing Science and}, address = {Stirling}, pages = {75 -- 87}, language = {en} } @inproceedings{Beyer, author = {Beyer, Dirk}, title = {Efficient Reachability Analysis and Refinement Checking of Timed Automata using BDDs}, series = {Correct hardware design and verification methods, 11th IFIP WG 10.5 advanced research working conference, proceedings, CHARME 2001, Livingston, Scotland, UK, September 4 - 7, 2001}, booktitle = {Correct hardware design and verification methods, 11th IFIP WG 10.5 advanced research working conference, proceedings, CHARME 2001, Livingston, Scotland, UK, September 4 - 7, 2001}, editor = {Margaria, Tiziana and Melham, Tom}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-42541-1}, pages = {86 -- 91}, language = {en} } @inproceedings{Beyer, author = {Beyer, Dirk}, title = {Improvements in BDD-based Reachability Analysis of Timed Automata}, series = {Formal methods for increasing software productivity, proceedings, FME 2001, International Symposium of Formal Methods Europe, Berlin, Germany, March 12 - 16, 2001}, booktitle = {Formal methods for increasing software productivity, proceedings, FME 2001, International Symposium of Formal Methods Europe, Berlin, Germany, March 12 - 16, 2001}, editor = {Zave, Pamela and Oliveira, Jos{\´e} Nuno}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-41791-5}, pages = {318 -- 343}, language = {en} } @inproceedings{BeyerLewerentzNoack, author = {Beyer, Dirk and Lewerentz, Claus and Noack, Andreas}, title = {Rabbit: A Tool for BDD-based Verification of Real-Time Systems}, series = {Computer aided verification, 15th international conference, proceedings, CAV 2003, Boulder, CO, USA, July 8 - 12, 2003}, booktitle = {Computer aided verification, 15th international conference, proceedings, CAV 2003, Boulder, CO, USA, July 8 - 12, 2003}, editor = {Hunt, Warren A.}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-40524-0}, pages = {122 -- 125}, 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.}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?}, series = {Formal techniques for networked and distributed systems - FORTE 2003, 23rd IFIP WG 6.1, international conference, Berlin, Germany, September 29 - October 2, 2003, proceedings}, booktitle = {Formal techniques for networked and distributed systems - FORTE 2003, 23rd IFIP WG 6.1, international conference, Berlin, Germany, September 29 - October 2, 2003, proceedings}, editor = {K{\"o}nig, Hartmut}, publisher = {Springer}, address = {Berlin [u.a.]}, isbn = {3-540-20175-0}, pages = {193 -- 208}, 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.}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {Clustering Software Artifacts Based on Frequent Common Changes}, series = {Proceedings, 13th International Workshop on Program Comprehension, IWPC 2005, 15 - 16 May 2005, St. Louis, Missouri}, booktitle = {Proceedings, 13th International Workshop on Program Comprehension, IWPC 2005, 15 - 16 May 2005, St. Louis, Missouri}, publisher = {IEEE Computer Society}, address = {Los Alamitos, Calif. [u.a.]}, isbn = {0-7695-2254-8}, pages = {259 -- 268}, language = {en} } @inproceedings{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {BDD-basierte Verifikation von Realzeit-Systemen}, language = {de} } @inproceedings{BeyerLewerentz, author = {Beyer, Dirk and Lewerentz, Claus}, title = {CrocoPat: Efficient Pattern Analysis in Object-Oriented Programs}, language = {en} } @inproceedings{BeyerNoackLewerentz, author = {Beyer, Dirk and Noack, Andreas and Lewerentz, Claus}, title = {Simple and Efficient Relational Querying of Software Structures}, series = {Proceedings, 10th Working Conference on Reverse Engineering, WCRE 2003, Victoria, B.C., Canada, 13 - 16 November 2003}, booktitle = {Proceedings, 10th Working Conference on Reverse Engineering, WCRE 2003, Victoria, B.C., Canada, 13 - 16 November 2003}, publisher = {IEEE Computer Society}, address = {Los Alamitos, Calif. [u.a.]}, isbn = {0-7695-2027-8}, pages = {216 -- 225}, abstract = {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.}, language = {en} } @article{BeyerNoackLewerentz, author = {Beyer, Dirk and Noack, Andreas and Lewerentz, Claus}, title = {Efficient Relational Calculation for Software Analysis}, language = {en} } @techreport{BeyerNoack, author = {Beyer, Dirk and Noack, Andreas}, title = {A Comparative Study of Decision Diagrams for Real-Time Verification}, publisher = {BTU, Institut f{\"u}r Informatik}, address = {Cottbus}, pages = {13}, 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 empirical and analytical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they explain the empirical results. Secondly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. Thirdly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-sized 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.}, language = {en} } @techreport{BeyerLewerentz, author = {Beyer, Dirk and Lewerentz, Claus}, title = {CrocoPat: A Tool for Efficient Pattern Recognition in Large Object-Oriented Programs}, publisher = {Inst. of Computer Science}, address = {Cottbus}, pages = {10}, language = {en} } @techreport{Beyer, author = {Beyer, Dirk}, title = {Reachability Analysis and Refinement Checking for BDD-based Model Checking of Timed Automata}, publisher = {Inst. of Computer Science}, address = {Cottbus}, pages = {12}, language = {en} } @techreport{Beyer, author = {Beyer, Dirk}, title = {Rabbit Verification of Real-Time Systems}, publisher = {Inst. of Computer Science}, address = {Cottbus}, pages = {4 Bl.}, language = {en} }