TY - THES A1 - Beyer, Dirk T1 - Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata KW - Formal Verification KW - Formal Method KW - Timed Automata KW - Reachability Analysis KW - BDD KW - Reactive Systems KW - Embedded Systems KW - Protocol Verification Y1 - 2002 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-000000258 UR - http://opus.kobv.de/btu/volltexte/2007/55/ ER - TY - RPRT A1 - Beyer, Dirk T1 - Rabbit Verification of Real-Time Systems Y1 - 2001 PB - Inst. of Computer Science CY - Cottbus ER - TY - RPRT A1 - Beyer, Dirk T1 - Reachability Analysis and Refinement Checking for BDD-based Model Checking of Timed Automata Y1 - 2001 PB - Inst. of Computer Science CY - Cottbus ER - TY - CHAP A1 - Beyer, Dirk A1 - Heinig, Andy ED - Rozenblit, Jerzy ED - Sveda, Miroslav ED - Rattray, Charles T1 - Different Strategies for BDD-based Reachability Analysis of Timed Automata T2 - Proceedings of the 2nd IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2001, Washington, D.C., April 2001) Y1 - 2001 SP - 89 EP - 98 CY - Stirling ER - TY - CHAP A1 - Beyer, Dirk A1 - Lewerentz, Claus A1 - Simon, Frank ED - Abran, Alain ED - Dumke, Reiner T1 - Impact of Inheritance on Metrics for Size, Coupling, and Cohesion in Object Oriented Systems T2 - New approaches in software measurement, 10th international workshop, proceedings, IWSM 2000, Berlin, Germany, October 4 - 6, 2000 Y1 - 2001 SN - 3-540-41727-3 SP - 1 EP - 17 PB - Springer CY - Berlin [u.a.] ER - TY - CHAP A1 - Beyer, Dirk A1 - Noack, Andreas ED - Ultes-Nitsche, Ulrich ED - Gnesi, Stefania T1 - Efficient Verification of Timed Automata using BDDs T2 - FMICS 2001, Formal methods for industrial critical systems, proceedings, International workshop on formal methods for industrial critical systems 6, 16 - 17 July 2001, Paris Y1 - 2001 SN - 2-7261-1187-4 SP - 95 EP - 113 PB - INRIA CY - Rocquencourt ER - TY - CHAP A1 - Beyer, Dirk A1 - Rust, Heinrich ED - Rattray, Charles ED - Sveda, Miroslav ED - Rozenblit, Jerzy T1 - Timed Automata Formal Definition and Semantics T2 - Joint Workshop on Formal Specification of Computer-Based Systems, Washington DC, USA, April 20, 2001 Y1 - 2001 SP - 75 EP - 87 PB - University of Stirling, Dept. of Computing Science and CY - Stirling ER - TY - CHAP A1 - Beyer, Dirk ED - Margaria, Tiziana ED - Melham, Tom T1 - Efficient Reachability Analysis and Refinement Checking of Timed Automata using BDDs T2 - 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 Y1 - 2001 SN - 3-540-42541-1 SP - 86 EP - 91 PB - Springer CY - Berlin [u.a.] ER - TY - CHAP A1 - Beyer, Dirk ED - Zave, Pamela ED - Oliveira, José Nuno T1 - Improvements in BDD-based Reachability Analysis of Timed Automata T2 - Formal methods for increasing software productivity, proceedings, FME 2001, International Symposium of Formal Methods Europe, Berlin, Germany, March 12 - 16, 2001 Y1 - 2001 SN - 3-540-41791-5 SP - 318 EP - 343 PB - Springer CY - Berlin [u.a.] ER - TY - CHAP A1 - Beyer, Dirk A1 - Lewerentz, Claus T1 - CrocoPat: Efficient Pattern Analysis in Object-Oriented Programs Y1 - 2003 ER - TY - RPRT A1 - Beyer, Dirk A1 - Lewerentz, Claus T1 - CrocoPat: A Tool for Efficient Pattern Recognition in Large Object-Oriented Programs Y1 - 2003 PB - Inst. of Computer Science CY - Cottbus ER - TY - CHAP A1 - Beyer, Dirk A1 - Lewerentz, Claus A1 - Noack, Andreas ED - Hunt, Warren A. T1 - Rabbit: A Tool for BDD-based Verification of Real-Time Systems T2 - Computer aided verification, 15th international conference, proceedings, CAV 2003, Boulder, CO, USA, July 8 - 12, 2003 N2 - 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. Y1 - 2003 SN - 3-540-40524-0 SP - 122 EP - 125 PB - Springer CY - Berlin [u.a.] ER - TY - RPRT A1 - Beyer, Dirk A1 - Noack, Andreas T1 - A Comparative Study of Decision Diagrams for Real-Time Verification N2 - 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. Y1 - 2003 PB - BTU, Institut für Informatik CY - Cottbus ER - TY - CHAP A1 - Beyer, Dirk A1 - Noack, Andreas ED - König, Hartmut T1 - Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification? T2 - Formal techniques for networked and distributed systems - FORTE 2003, 23rd IFIP WG 6.1, international conference, Berlin, Germany, September 29 - October 2, 2003, proceedings N2 - 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. Y1 - 2003 SN - 3-540-20175-0 SP - 193 EP - 208 PB - Springer CY - Berlin [u.a.] ER - TY - CHAP A1 - Beyer, Dirk A1 - Noack, Andreas A1 - Lewerentz, Claus T1 - Simple and Efficient Relational Querying of Software Structures T2 - Proceedings, 10th Working Conference on Reverse Engineering, WCRE 2003, Victoria, B.C., Canada, 13 - 16 November 2003 N2 - 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. Y1 - 2003 SN - 0-7695-2027-8 SP - 216 EP - 225 PB - IEEE Computer Society CY - Los Alamitos, Calif. [u.a.] ER - TY - CHAP A1 - Beyer, Dirk A1 - Noack, Andreas T1 - Clustering Software Artifacts Based on Frequent Common Changes T2 - Proceedings, 13th International Workshop on Program Comprehension, IWPC 2005, 15 - 16 May 2005, St. Louis, Missouri Y1 - 2005 SN - 0-7695-2254-8 SP - 259 EP - 268 PB - IEEE Computer Society CY - Los Alamitos, Calif. [u.a.] ER - TY - CHAP A1 - Beyer, Dirk A1 - Noack, Andreas T1 - BDD-basierte Verifikation von Realzeit-Systemen Y1 - 2000 ER - TY - JOUR A1 - Beyer, Dirk A1 - Noack, Andreas A1 - Lewerentz, Claus T1 - Efficient Relational Calculation for Software Analysis Y1 - 2005 ER -