Publications of year 2001

Articles in conference or workshop proceedings

  1. 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 4-7), LNCS 2144, pages 86-91, 2001. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    For the formal specification and verification of real-time systems we use the modular formalism Cottbus Timed Automata (CTA), which is an extension of timed automata [AD94]. Matrix-based algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDD-based version of Rabbit, which supports also refinement checking, is now available.
    Annotation:
    CHARME 2001, Livingston, September 4-7,
    Tiziana Margaria, Tom Melham, editors.
    © 2006 Springer-Verlag
    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 4-7)},
    editor = {T.~Margaria and T.~F.~Melham},
    series = {LNCS~2144},
    pages = {86-91},
    publisher = {Springer-Verlag, Heidelberg},
    year = {2001},
    isbn = {3-540-42541-1},
    keyword = {Formal Verification of Real-Time Systems},
    pdf = {https://www.sosy-lab.org/research/pub/2001-CHARME.Efficient_Reachability_Analysis_and_Refinement_Checking_of_Timed_Automata_using_BDDs.pdf},
    url = {},
    abstract = { For the formal specification and verification of real-time systems we use the modular formalism Cottbus Timed Automata (CTA), which is an extension of timed automata [AD94]. Matrix-based algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDD-based version of Rabbit, which supports also refinement checking, is now available. },
    annote = { CHARME 2001, Livingston, September 4-7,
    Tiziana Margaria, Tom Melham, editors.
    © 2006 Springer-Verlag
    Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
    Decribes how the tool checks refinement via simulation relation. }, }

  2. Dirk Beyer. Improvements in BDD-Based 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 12-16): Formal Methods for Increasing Software Productivity, LNCS 2021, pages 318-343, 2001. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Formal Verification of Real-Time 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 BDD-based 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 real-time models, which have a good-natured communication structure.
    Annotation:
    FME 2001, Berlin, March 12-16,
    Jose Nuno Oliveira, Pamela Zave, editors.
    © 2006 Springer-Verlag
    Online: http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm
    Discretization of Timed Automata, BDD-based 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 12-16): Formal Methods for Increasing Software Productivity},
    editor = {J.~N.~Oliveira and P.~Zave},
    series = {LNCS~2021},
    pages = {318-343},
    publisher = {Springer-Verlag, Heidelberg},
    year = {2001},
    isbn = {3-540-41791-5},
    keyword = {Formal Verification of Real-Time Systems},
    pdf = {https://www.sosy-lab.org/research/pub/2001-FME.Improvements_in_BDD-Based_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 BDD-based 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 real-time models, which have a good-natured communication structure. },
    annote = { FME 2001, Berlin, March 12-16,
    Jose Nuno Oliveira, Pamela Zave, editors.
    © 2006 Springer-Verlag
    Online: http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm
    Discretization of Timed Automata, BDD-based 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. }, }

  3. Dirk Beyer. Rabbit: Verification of Real-Time Systems. In P. Pettersson and S. Yovine, editors, Proceedings of the Workshop on Real-Time Tools (RT-TOOLS 2001, Aalborg, August 20), Uppsala, pages 13-21, 2001. [ PDF ] Keyword(s): Formal Verification of Real-Time 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 BDD-based 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.
    Annotation:
    RT-TOOLS 2001, Aalborg, August 20
    Paul Pettersson, Sergio Yovine, editors

    @InProceedings{RT-TOOLS01,
    author = {Dirk Beyer},
    title = {Rabbit: Verification of Real-Time Systems},
    booktitle = {Proceedings of the Workshop on Real-Time Tools (RT-TOOLS~2001, Aalborg, August 20)},
    editor = {P.~Pettersson and S.~Yovine},
    pages = {13-21},
    address = {Uppsala},
    year = {2001},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    pdf = {https://www.sosy-lab.org/research/pub/2001-RT-TOOLS.Rabbit_Verification_of_Real-Time_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 BDD-based 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 = {RT-TOOLS 2001, Aalborg, August 20 
    Paul Pettersson, Sergio Yovine, editors}, }

  4. Dirk Beyer and Andy Heinig. Different Strategies for BDD-Based 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 Computer-Based Systems (FSCBS 2001, Washington, D.C., April 20), Stirling, pages 89-98, 2001. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    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 Computer-Based Systems (FSCBS~2001, Washington, D.C., April 20)},
    editor = {C.~Rattray and M.~Sveda and J.~Rozenblit},
    pages = {89-98},
    address = {Stirling},
    year = {2001},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    annote = {FSCBS 2001, Washington, D.C., April 20 
    Charles Rattray, Miroslav Sveda, Jerzy Rozenblit, editors}, }

  5. 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 4-6): New Approaches in Software Measurement, LNCS 2006, pages 1-17, 2001. Springer-Verlag, Heidelberg. [ PDF ] 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.
    Annotation:
    Online: http://link.springer.de/link/service/series/0558/bibs/2006/20060001.htm

    @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 4-6): New Approaches in Software Measurement},
    editor = {R.~Dumke and A.~Abran},
    series = {LNCS~2006},
    pages = {1-17},
    publisher = {Springer-Verlag, Heidelberg},
    year = {2001},
    isbn = {3-540-41727-3},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2000-IWSM.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 4-6,
    Reiner Dumke, Alain Abran, editors.
    © 2006 Springer-Verlag}, annote = { Online: http://link.springer.de/link/service/series/0558/bibs/2006/20060001.htm
    }, }

  6. Dirk Beyer and Andreas Noack. Efficient Verification of Timed Automata using BDDs. In S. Gnesi and U. Ultes-Nitsche, editors, Proceedings of the Sixth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2001, Paris, July 16-17), pages 95-113, 2001. INRIA, Paris. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time 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 on-the-fly algorithm and refinement checking for large models.
    Annotation:
    FMICS 2001, Paris, July 16-17
    Stefania Gnesi, Ulrich Ultes-Nitsche, 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 16-17)},
    editor = {S.~Gnesi and U.~Ultes-Nitsche},
    pages = {95-113},
    publisher = {INRIA, Paris},
    year = {2001},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    ps = {https://www.sosy-lab.org/research/pub/2001-FMICS.Efficient_Verification_of_Timed_Automata_using_BDDs.ps},
    pdf = {https://www.sosy-lab.org/research/pub/2001-FMICS.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 on-the-fly algorithm and refinement checking for large models. },
    annote = {FMICS 2001, Paris, July 16-17 
    Stefania Gnesi, Ulrich Ultes-Nitsche, editors}, }

  7. 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 Computer-Based Systems (FSCBS 2001, Washington, D.C., April 20), Stirling, pages 75-87, 2001. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time 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 write-access to signals and variables.
    Annotation:
    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 Computer-Based Systems (FSCBS~2001, Washington, D.C., April 20)},
    editor = {C.~Rattray and M.~Sveda and J.~Rozenblit},
    pages = {75-87},
    address = {Stirling},
    year = {2001},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    ps = {https://www.sosy-lab.org/research/pub/2001-FSCBS.Cottbus_Timed_Automata_Formal_Definition_and_Compositional_Semantics.revised.ps},
    pdf = {https://www.sosy-lab.org/research/pub/2001-FSCBS.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 write-access 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

  1. Dirk Beyer. Rabbit: Verification of Real-Time Systems. Technical report I-05/2001, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, March 2001. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See CAV03 [25] for proceedings version.

    @TechReport{TR05-BTU01,
    author = {Dirk Beyer},
    title = {Rabbit: Verification of Real-Time Systems},
    institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus},
    month = {March},
    year = {2001},
    number = {I-05/2001},
    keyword = {Formal Verification of Real-Time Systems},
    annote = {See CAV03 [25] for proceedings version.},
    
    }
    

  2. Dirk Beyer. Reachability Analysis and Refinement Checking for BDD-Based Model Checking of Timed Automata. Technical report I-04/2001, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, February 2001. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See CHARME01 [20] for proceedings version.

    @TechReport{TR04-BTU01,
    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 = {I-04/2001},
    keyword = {Formal Verification of Real-Time 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: Mon Dec 18 13:27:46 2017


This document was translated from BibTEX by bibtex2html