Publications of year 2001
Articles in conference or workshop proceedings

Dirk Beyer.
Efficient Reachability Analysis and Refinement Checking of Timed Automata using BDDs.
In T. Margaria and T. F. Melham, editors, Proceedings of the 11th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2001, Livingston, September 47), LNCS 2144, pages 8691, 2001.
SpringerVerlag, Heidelberg.
[ Article ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
For the formal specification and verification of realtime systems we use the modular formalism Cottbus Timed Automata (CTA), which is an extension of timed automata [AD94]. Matrixbased algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDDbased version of Rabbit, which supports also refinement checking, is now available.CHARME 2001, Livingston, September 47,
Tiziana Margaria, Tom Melham, editors.
© 2006 SpringerVerlag
Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
Decribes how the tool checks refinement via simulation relation.@InProceedings{CHARME01, author = {Dirk Beyer}, title = {Efficient Reachability Analysis and Refinement Checking of Timed Automata using {BDD}s}, booktitle = {Proceedings of the 11th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME~2001, Livingston, September 47)}, editor = {T.~Margaria and T.~F.~Melham}, series = {LNCS~2144}, pages = {8691}, publisher = {SpringerVerlag, Heidelberg}, year = {2001}, isbn = {3540425411}, keyword = {Formal Verification of RealTime Systems}, pdf = {https://www.sosylab.org/research/pub/2001CHARME.Efficient_Reachability_Analysis_and_Refinement_Checking_of_Timed_Automata_using_BDDs.pdf}, url = {}, abstract = { For the formal specification and verification of realtime systems we use the modular formalism Cottbus Timed Automata (CTA), which is an extension of timed automata [AD94]. Matrixbased algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDDbased version of Rabbit, which supports also refinement checking, is now available. }, annote = { CHARME 2001, Livingston, September 47,
Tiziana Margaria, Tom Melham, editors.
© 2006 SpringerVerlag
Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
Decribes how the tool checks refinement via simulation relation. }, } 
Dirk Beyer.
Improvements in BDDBased Reachability Analysis of Timed Automata.
In J. N. Oliveira and P. Zave, editors, Proceedings of the Tenth International Symposium of Formal Methods Europe (FME 2001, Berlin, March 1216): Formal Methods for Increasing Software Productivity, LNCS 2021, pages 318343, 2001.
SpringerVerlag, Heidelberg.
[ Article ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
To develop efficient algorithms for the reachability analysis of timed automata, a promising approach is to use binary decision diagrams (BDDs) as data structure for the representation of the explored state space. The size of a BDD is very sensitive to the ordering of the variables. We use the communication structure to deduce an estimation for the BDD size. In our experiments, this guides the choice of good variable orderings, which leads to an efficient reachability analysis. We develop a discrete semantics for closed timed automata to get a finite state space required by the BDDbased representation and we prove the equivalence to the continuous semantics regarding the set of reachable locations. An upper bound for the size of the BDD representing the transition relation and an estimation for the set of reachable configurations based on the communication structure is given. We implemented these concepts in the verification tool Rabbit [BR00]. Different case studies justify our conjecture: Polynomial reachability analysis seems to be possible for some classes of realtime models, which have a goodnatured communication structure.FME 2001, Berlin, March 1216,
Jose Nuno Oliveira, Pamela Zave, editors.
© 2006 SpringerVerlag
Online: http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm
Discretization of Timed Automata, BDDbased representation, proof of an upper bound for the BDD of the transition relation, BDD variable ordering, heuristics for efficient verification, contains the proof of the equivalence of our integer semantics to the continuous semantics regarding reachable locations.@InProceedings{FME01, author = {Dirk Beyer}, title = {Improvements in {BDD}Based Reachability Analysis of Timed Automata}, booktitle = {Proceedings of the Tenth International Symposium of Formal Methods Europe (FME~2001, Berlin, March 1216): Formal Methods for Increasing Software Productivity}, editor = {J.~N.~Oliveira and P.~Zave}, series = {LNCS~2021}, pages = {318343}, publisher = {SpringerVerlag, Heidelberg}, year = {2001}, isbn = {3540417915}, keyword = {Formal Verification of RealTime Systems}, pdf = {https://www.sosylab.org/research/pub/2001FME.Improvements_in_BDDBased_Reachability_Analysis_of_Timed_Automata.pdf}, url = {}, abstract = { To develop efficient algorithms for the reachability analysis of timed automata, a promising approach is to use binary decision diagrams (BDDs) as data structure for the representation of the explored state space. The size of a BDD is very sensitive to the ordering of the variables. We use the communication structure to deduce an estimation for the BDD size. In our experiments, this guides the choice of good variable orderings, which leads to an efficient reachability analysis. We develop a discrete semantics for closed timed automata to get a finite state space required by the BDDbased representation and we prove the equivalence to the continuous semantics regarding the set of reachable locations. An upper bound for the size of the BDD representing the transition relation and an estimation for the set of reachable configurations based on the communication structure is given. We implemented these concepts in the verification tool Rabbit [BR00]. Different case studies justify our conjecture: Polynomial reachability analysis seems to be possible for some classes of realtime models, which have a goodnatured communication structure. }, annote = { FME 2001, Berlin, March 1216,
Jose Nuno Oliveira, Pamela Zave, editors.
© 2006 SpringerVerlag
Online: http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm
Discretization of Timed Automata, BDDbased representation, proof of an upper bound for the BDD of the transition relation, BDD variable ordering, heuristics for efficient verification, contains the proof of the equivalence of our integer semantics to the continuous semantics regarding reachable locations. }, } 
Dirk Beyer.
Rabbit: Verification of RealTime Systems.
In P. Pettersson and S. Yovine, editors, Proceedings of the Workshop on RealTime Tools (RTTOOLS 2001, Aalborg, August 20), Uppsala, pages 1321, 2001.
[ Article ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
This paper gives a short overview of a model checking tool for Cottbus Timed Automata, which is a modular modeling language based on timed and hybrid automata. For timed automata, the current version of the tool provides BDDbased verification using an integer semantics. Reachability analysis as well as refinement checking is possible. To find good variable orderings it uses the component structure of the model and an upper bound for the BDD size. For hybrid automata, reachability analysis based on the double description method is implemented.RTTOOLS 2001, Aalborg, August 20
Paul Pettersson, Sergio Yovine, editors@InProceedings{RTTOOLS01, author = {Dirk Beyer}, title = {Rabbit: Verification of RealTime Systems}, booktitle = {Proceedings of the Workshop on RealTime Tools (RTTOOLS~2001, Aalborg, August 20)}, editor = {P.~Pettersson and S.~Yovine}, pages = {1321}, address = {Uppsala}, year = {2001}, isbn = {}, keyword = {Formal Verification of RealTime Systems}, pdf = {https://www.sosylab.org/research/pub/2001RTTOOLS.Rabbit_Verification_of_RealTime_Systems.pdf}, abstract = { This paper gives a short overview of a model checking tool for Cottbus Timed Automata, which is a modular modeling language based on timed and hybrid automata. For timed automata, the current version of the tool provides BDDbased verification using an integer semantics. Reachability analysis as well as refinement checking is possible. To find good variable orderings it uses the component structure of the model and an upper bound for the BDD size. For hybrid automata, reachability analysis based on the double description method is implemented. }, annote = {RTTOOLS 2001, Aalborg, August 20
Paul Pettersson, Sergio Yovine, editors}, } 
Dirk Beyer and Andy Heinig.
Different Strategies for BDDBased Reachability Analysis of Timed Automata.
In C. Rattray, M. Sveda, and J. Rozenblit, editors, Proceedings of the Second IEEE/IFIP Joint Workshop on Formal Specifications of ComputerBased Systems (FSCBS 2001, Washington, D.C., April 20), Stirling, pages 8998, 2001.
Keyword(s): Formal Verification of RealTime Systems.
FSCBS 2001, Washington, D.C., April 20
Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors@InProceedings{FSCBS01b, author = {Dirk Beyer and Andy Heinig}, title = {Different Strategies for {BDD}Based Reachability Analysis of Timed Automata}, booktitle = {Proceedings of the Second IEEE/IFIP Joint Workshop on Formal Specifications of ComputerBased Systems (FSCBS~2001, Washington, D.C., April 20)}, editor = {C.~Rattray and M.~Sveda and J.~Rozenblit}, pages = {8998}, address = {Stirling}, year = {2001}, isbn = {}, keyword = {Formal Verification of RealTime Systems}, annote = {FSCBS 2001, Washington, D.C., April 20
Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors}, } 
Dirk Beyer,
Claus Lewerentz,
and Frank Simon.
Impact of Inheritance on Metrics for Size, Coupling, and Cohesion in Object Oriented Systems.
In R. Dumke and A. Abran, editors, Proceedings of the Tenth International Workshop on Software Measurement (IWSM 2000, Berlin, October 46): New Approaches in Software Measurement, LNCS 2006, pages 117, 2001.
SpringerVerlag, Heidelberg.
[ Article ] Keyword(s): Structural Analysis and Comprehension.
Abstract
In today's engineering of object oriented systems many different metrics are used to get feedback about design quality and to automatically identify design weaknesses. While the concept of inheritance is covered by special inheritance metrics its impact on other classical metrics (like size, coupling or cohesion metrics) is not considered; this can yield misleading measurement values and false interpretations. In this paper we present an approach to work the concept of inheritance into classical metrics (and with it the related concepts of overriding, overloading and polymorphism). This is done by some language dependent flattening functions that modify the data on which the measurement will be done. These functions are implemented within our metrics tool Crocodile and are applied for a case study: the comparison of the measurement values of the original data with the measurement values of the flattened data yields interesting results and improves the power of classical measurements for interpretation.@InProceedings{IWSM00, author = {Dirk Beyer and Claus Lewerentz and Frank Simon}, title = {Impact of Inheritance on Metrics for Size, Coupling, and Cohesion in Object Oriented Systems}, booktitle = {Proceedings of the Tenth International Workshop on Software Measurement (IWSM~2000, Berlin, October 46): New Approaches in Software Measurement}, editor = {R.~Dumke and A.~Abran}, series = {LNCS~2006}, pages = {117}, publisher = {SpringerVerlag, Heidelberg}, year = {2001}, isbn = {3540417273}, keyword = {Structural Analysis and Comprehension}, pdf = {https://www.sosylab.org/research/pub/2000IWSM.Impact_of_Inheritance_on_Metrics.pdf}, url = {}, abstract = { In today's engineering of object oriented systems many different metrics are used to get feedback about design quality and to automatically identify design weaknesses. While the concept of inheritance is covered by special inheritance metrics its impact on other classical metrics (like size, coupling or cohesion metrics) is not considered; this can yield misleading measurement values and false interpretations. In this paper we present an approach to work the concept of inheritance into classical metrics (and with it the related concepts of overriding, overloading and polymorphism). This is done by some language dependent flattening functions that modify the data on which the measurement will be done. These functions are implemented within our metrics tool Crocodile and are applied for a case study: the comparison of the measurement values of the original data with the measurement values of the flattened data yields interesting results and improves the power of classical measurements for interpretation. }, annote = {IWSM 2000, Berlin, October 46,
Reiner Dumke, Alain Abran, editors.
© 2006 SpringerVerlag}, annote = { Online: http://link.springer.de/link/service/series/0558/bibs/2006/20060001.htm
}, } 
Dirk Beyer and Andreas Noack.
Efficient Verification of Timed Automata using BDDs.
In S. Gnesi and U. UltesNitsche, editors, Proceedings of the Sixth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2001, Paris, July 1617), pages 95113, 2001.
INRIA, Paris.
[ Article ] [ Presentation ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
This paper investigates the efficient reachability analysis of timed automata. It describes a discretization of time which preserves the reachability properties. The discretization allows to represent sets of configurations of timed automata as binary decision diagrams (BDDs). Further techniques, like computing good variable orderings, are applied to use the full potential of BDDs as compact and canonical representation of large sets. We implemented these concepts within the tool Rabbit. The highly improved performance is shown for some example models. For additional speedup we used an onthefly algorithm and refinement checking for large models.FMICS 2001, Paris, July 1617
Stefania Gnesi, Ulrich UltesNitsche, editors@InProceedings{FMICS01, author = {Dirk Beyer and Andreas Noack}, title = {Efficient Verification of Timed Automata using {BDD}s}, booktitle = {Proceedings of the Sixth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS~2001, Paris, July 1617)}, editor = {S.~Gnesi and U.~UltesNitsche}, pages = {95113}, publisher = {INRIA, Paris}, year = {2001}, isbn = {}, keyword = {Formal Verification of RealTime Systems}, ps = {https://www.sosylab.org/research/pub/2001FMICS.Efficient_Verification_of_Timed_Automata_using_BDDs.ps}, pdf = {https://www.sosylab.org/research/pub/2001FMICS.Efficient_Verification_of_Timed_Automata_using_BDDs.pdf}, abstract = { This paper investigates the efficient reachability analysis of timed automata. It describes a discretization of time which preserves the reachability properties. The discretization allows to represent sets of configurations of timed automata as binary decision diagrams (BDDs). Further techniques, like computing good variable orderings, are applied to use the full potential of BDDs as compact and canonical representation of large sets. We implemented these concepts within the tool Rabbit. The highly improved performance is shown for some example models. For additional speedup we used an onthefly algorithm and refinement checking for large models. }, annote = {FMICS 2001, Paris, July 1617
Stefania Gnesi, Ulrich UltesNitsche, editors}, } 
Dirk Beyer and Heinrich Rust.
Cottbus Timed Automata: Formal Definition and Semantics.
In C. Rattray, M. Sveda, and J. Rozenblit, editors, Proceedings of the Second IEEE/IFIP Joint Workshop on Formal Specifications of ComputerBased Systems (FSCBS 2001, Washington, D.C., April 20), Stirling, pages 7587, 2001.
[ Article ] [ Presentation ] Keyword(s): Formal Verification of RealTime Systems.
Abstract
We present a formalism for modular modelling of hybrid systems, the Cottbus Timed Automata. For the theoretical basis, we build on work about timed and hybrid automata. We use concepts from concurrency theory to model communication of separately defined modules, but we extend these concepts to be able to express explicitly read and writeaccess to signals and variables.FSCBS 2001, Washington, D.C., April 20
Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors
The pdf is a revised version of the original paper.
The full formal definition and semantics of CTA.@InProceedings{FSCBS01a, author = {Dirk Beyer and Heinrich Rust}, title = {{C}ottbus {T}imed {A}utomata: Formal Definition and Semantics}, booktitle = {Proceedings of the Second IEEE/IFIP Joint Workshop on Formal Specifications of ComputerBased Systems (FSCBS~2001, Washington, D.C., April 20)}, editor = {C.~Rattray and M.~Sveda and J.~Rozenblit}, pages = {7587}, address = {Stirling}, year = {2001}, isbn = {}, keyword = {Formal Verification of RealTime Systems}, ps = {https://www.sosylab.org/research/pub/2001FSCBS.Cottbus_Timed_Automata_Formal_Definition_and_Compositional_Semantics.revised.ps}, pdf = {https://www.sosylab.org/research/pub/2001FSCBS.Cottbus_Timed_Automata_Formal_Definition_and_Compositional_Semantics.revised.pdf}, abstract = { We present a formalism for modular modelling of hybrid systems, the Cottbus Timed Automata. For the theoretical basis, we build on work about timed and hybrid automata. We use concepts from concurrency theory to model communication of separately defined modules, but we extend these concepts to be able to express explicitly read and writeaccess to signals and variables. }, annote = {FSCBS 2001, Washington, D.C., April 20
Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors
The pdf is a revised version of the original paper.
The full formal definition and semantics of CTA.}, }
Internal reports

Dirk Beyer.
Rabbit: Verification of RealTime Systems.
Technical report I05/2001, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, March 2001.
Keyword(s): Formal Verification of RealTime Systems.
See CAV03 [25] for proceedings version.@TechReport{TR05BTU01, author = {Dirk Beyer}, title = {Rabbit: Verification of RealTime Systems}, institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {March}, year = {2001}, number = {I05/2001}, keyword = {Formal Verification of RealTime Systems}, annote = {See CAV03 [25] for proceedings version.}, }

Dirk Beyer.
Reachability Analysis and Refinement Checking for BDDBased Model Checking of Timed Automata.
Technical report I04/2001, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, February 2001.
Keyword(s): Formal Verification of RealTime Systems.
See CHARME01 [20] for proceedings version.@TechReport{TR04BTU01, author = {Dirk Beyer}, title = {Reachability Analysis and Refinement Checking for {BDD}Based Model Checking of Timed Automata}, institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {February}, year = {2001}, number = {I04/2001}, keyword = {Formal Verification of RealTime Systems}, annote = {See CHARME01 [20] 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: Thu Feb 21 20:21:15 2019
This document was translated from BibT_{E}X by bibtex2html