Publications of year 2001
Articles in conference or workshop proceedings

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.
doi:10.1007/3540447989_6
Keyword(s):
Formal Verification of RealTime Systems
Publisher's Version
PDF
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.BibTeX Entry
@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}, pages = {8691}, year = {2001}, series = {LNCS~2144}, publisher = {SpringerVerlag, Heidelberg}, isbn = {3540425411}, doi = {10.1007/3540447989_6}, url = {}, pdf = {https://www.sosylab.org/research/pub/2001CHARME.Efficient_Reachability_Analysis_and_Refinement_Checking_of_Timed_Automata_using_BDDs.pdf}, 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.}, keyword = {Formal Verification of RealTime Systems}, annote = {Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
Decribes how the tool checks refinement via simulation relation.}, }Additional Infos
Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
Decribes how the tool checks refinement via simulation relation. 
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.
doi:10.1007/3540452516_18
Keyword(s):
Formal Verification of RealTime Systems
Publisher's Version
PDF
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.BibTeX Entry
@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}, pages = {318343}, year = {2001}, series = {LNCS~2021}, publisher = {SpringerVerlag, Heidelberg}, isbn = {3540417915}, doi = {10.1007/3540452516_18}, url = {}, pdf = {https://www.sosylab.org/research/pub/2001FME.Improvements_in_BDDBased_Reachability_Analysis_of_Timed_Automata.pdf}, 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.}, keyword = {Formal Verification of RealTime Systems}, annote = {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.}, }Additional Infos
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. 
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.
doi:10.1007/3540447040_1
Keyword(s):
Structural Analysis and Comprehension
Publisher's Version
PDF
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.BibTeX Entry
@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}, pages = {117}, year = {2001}, series = {LNCS~2006}, publisher = {SpringerVerlag, Heidelberg}, isbn = {3540417273}, doi = {10.1007/3540447040_1}, url = {}, pdf = {https://www.sosylab.org/research/pub/2000IWSM.Impact_of_Inheritance_on_Metrics.pdf}, 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.}, keyword = {Structural Analysis and Comprehension}, annote = {Online: http://link.springer.de/link/service/series/0558/bibs/2006/20060001.htm
}, }Additional Infos

Rabbit: Verification of RealTime Systems.
In P. Pettersson and
S. Yovine, editors,
Proceedings of the Workshop on RealTime Tools
(RTTOOLS 2001, Aalborg, August 20),
pages 1321,
2001.
Keyword(s):
Formal 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.BibTeX Entry
@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}, year = {2001}, isbn = {}, 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.}, keyword = {Formal Verification of RealTime Systems}, address = {Uppsala}, annote = {}, doinone = {DOI not available}, } 
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.
Keyword(s):
Formal Verification of RealTime Systems
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.BibTeX Entry
@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}, year = {2001}, publisher = {INRIA, Paris}, isbn = {}, 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.}, keyword = {Formal Verification of RealTime Systems}, annote = {}, doinone = {DOI not available}, } 
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),
pages 8998,
2001.
Keyword(s):
Formal Verification of RealTime Systems
BibTeX Entry
@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}, year = {2001}, isbn = {}, keyword = {Formal Verification of RealTime Systems}, address = {Stirling}, annote = {}, doinone = {DOI not available}, } 
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),
pages 7587,
2001.
Keyword(s):
Formal Verification of RealTime Systems
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.BibTeX Entry
@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}, year = {2001}, isbn = {}, 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.}, keyword = {Formal Verification of RealTime Systems}, address = {Stirling}, annote = {The pdf is a revised version of the original paper.
The full formal definition and semantics of CTA.}, doinone = {DOI not available}, }Additional Infos
The pdf is a revised version of the original paper.
The full formal definition and semantics of CTA.
Internal reports

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
BibTeX Entry
@techreport{TR05BTU01, author = {Dirk Beyer}, title = {Rabbit: Verification of RealTime Systems}, number = {I05/2001}, year = {2001}, keyword = {Formal Verification of RealTime Systems}, annote = {See CAV03 [25] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {March}, }Additional Infos
See CAV03 [25] for proceedings version. 
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
BibTeX Entry
@techreport{TR04BTU01, author = {Dirk Beyer}, title = {Reachability Analysis and Refinement Checking for {BDD}Based Model Checking of Timed Automata}, number = {I04/2001}, year = {2001}, keyword = {Formal Verification of RealTime Systems}, annote = {See CHARME01 [20] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {February}, }Additional Infos
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.