Publications of year 2000

Articles in conference or workshop proceedings

  1. Dirk Beyer, Claus Lewerentz, and Heinrich Rust. Modelling and Analysing a Railroad Crossing in a Modular Way. In S. Gnesi, I. Schieferdecker, and A. Rennoch, editors, Proceedings of the Fifth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2000, Berlin, April 3-4), Berlin, pages 287-303, 2000. [ PDF ] [ PS ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    One problem of modelling hybrid systems with existing notations of hybrid automata is that there is no modular structure in the model. We introduce an extended modelling notation which allows the modelling of a system as a hierarchical structure of modules. The modules are capable of communicating through the elements of an explicitly defined interface. The interface consists of signals and variables declared with different access modes. This paper describes a model of the railroad crossing example and how to verify it. The current version of a tool for reachability analysis using the double description method to represent symbolically the sets of reachable configurations is presented.
    Annotation:
    FMICS 2000, Berlin, April 3-4
    Stefania Gnesi, Ina Schieferdecker, Axel Rennoch, editors
    Describes a case study for modeling and analysis using the DDM-based representation.

    @InProceedings{FMICS00,
    author = {Dirk Beyer and Claus Lewerentz and Heinrich Rust},
    title = {Modelling and Analysing a Railroad Crossing in a Modular Way},
    booktitle = {Proceedings of the Fifth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS~2000, Berlin, April 3-4)},
    editor = {S.~Gnesi and I.~Schieferdecker and A.~Rennoch},
    year = {2000},
    pages = {287-303},
    address = {Berlin},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    ps = {https://www.sosy-lab.org/research/pub/2000-FMICS.Modelling_and_Analysing_a_Railroad_Crossing_in_a_Modular_Way.ps},
    pdf = {https://www.sosy-lab.org/research/pub/2000-FMICS.Modelling_and_Analysing_a_Railroad_Crossing_in_a_Modular_Way.pdf},
    abstract = { One problem of modelling hybrid systems with existing notations of hybrid automata is that there is no modular structure in the model. We introduce an extended modelling notation which allows the modelling of a system as a hierarchical structure of modules. The modules are capable of communicating through the elements of an explicitly defined interface. The interface consists of signals and variables declared with different access modes. This paper describes a model of the railroad crossing example and how to verify it. The current version of a tool for reachability analysis using the double description method to represent symbolically the sets of reachable configurations is presented. },
    annote = {FMICS 2000, Berlin, April 3-4 
    Stefania Gnesi, Ina Schieferdecker, Axel Rennoch, editors
    Describes a case study for modeling and analysis using the DDM-based representation.}, }

  2. Dirk Beyer and Andreas Noack. BDD-basierte Verifikation von Realzeit-Systemen. In J. Grabowski and S. Heymer, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT 2000, Lübeck, June 22-23), pages 79-89, 2000. Shaker Verlag, Aachen. [ PDF ] Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    Diese Arbeit behandelt die effiziente Erreichbarkeitsanalyse von Timed Automata. Wir beschreiben eine Erreichbarkeitseigenschaften erhaltende Diskretisierung der Zeit. Diese ermöglicht es, Konfigurationsmengen von Timed Automata als Binary Decision Diagrams (BDDs) darzustellen. Die kompakte BDD-Repräsentation großer Mengen erfordert geeignete Variablenordnungen. Zur deren Bestimmung nutzen wir Strukturinformationen aus der Modellierungsnotation Cottbus Timed Automaton. Wir belegen die erzielten Effizienzverbesserungen durch Meßwerte.
    Annotation:
    FBT 2000, Lübeck, June 22-23
    Jens Grabowski, Stefan Heymer, editors

    @InProceedings{FBT00,
    author = {Dirk Beyer and Andreas Noack},
    title = {{BDD}-basierte {V}erifikation von {R}ealzeit-{S}ystemen},
    booktitle = {Tagungsband Formale Beschreibungstechniken f{\"u}r verteilte Systeme (FBT~2000, L{\"u}beck, June 22-23)},
    editor = {J.~Grabowski and S.~Heymer},
    pages = {79-89},
    year = {2000},
    publisher = {Shaker Verlag, Aachen},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    pdf = {https://www.sosy-lab.org/research/pub/2000-FBT.BDD-basierte_Verifikation_von_Realzeit-Systemen.pdf},
    abstract = { Diese Arbeit behandelt die effiziente Erreichbarkeitsanalyse von Timed Automata. Wir beschreiben eine Erreichbarkeitseigenschaften erhaltende Diskretisierung der Zeit. Diese ermöglicht es, Konfigurationsmengen von Timed Automata als Binary Decision Diagrams (BDDs) darzustellen. Die kompakte BDD-Repräsentation großer Mengen erfordert geeignete Variablenordnungen. Zur deren Bestimmung nutzen wir Strukturinformationen aus der Modellierungsnotation Cottbus Timed Automaton. Wir belegen die erzielten Effizienzverbesserungen durch Meßwerte. },
    annote = {FBT 2000, Lübeck, June 22-23 
    Jens Grabowski, Stefan Heymer, editors}, }

  3. Dirk Beyer and Heinrich Rust. A Tool for Modular Modelling and Verification of Hybrid Systems. In A. Crespo and J. Vila, editors, Proceedings of the 25th IFAC/IFIP Workshop on Real-Time Programming (WRTP 2000, Palma, May 17-19), pages 169-174, 2000. Elsevier Science, Oxford. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    WRTP 2000, Palma, May 17-19
    Alfons Crespo, Joan Vila, editors
    Also as preprint: Proc. WRTP'00, pages 181-186, Valencia, 2000.
    The reference for the first version of the tool using the double decription method (DDM) for hybrid systems.

    @InProceedings{WRTP00,
    author = {Dirk Beyer and Heinrich Rust},
    title = {A Tool for Modular Modelling and Verification of Hybrid Systems},
    booktitle = {Proceedings of the 25th IFAC/IFIP Workshop on Real-Time Programming (WRTP~2000, Palma, May 17-19)},
    year = {2000},
    editor = {A.~Crespo and J.~Vila},
    pages = {169-174},
    publisher = {Elsevier Science, Oxford},
    isbn = {0-08-043686-2},
    url = {},
    keyword = {Formal Verification of Real-Time Systems},
    annote = {WRTP 2000, Palma, May 17-19 
    Alfons Crespo, Joan Vila, editors
    Also as preprint: Proc. WRTP'00, pages 181-186, Valencia, 2000.
    The reference for the first version of the tool using the double decription method (DDM) for hybrid systems.}, }

  4. Dirk Beyer and Heinrich Rust. Modular Modelling and Verification with Cottbus Timed Automata. In C. Rattray and M. Sveda, editors, Proceedings of the IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS 2000, Edinburgh, April 6-7), Stirling, pages 17-24, 2000. Keyword(s): Formal Verification of Real-Time Systems.
    Abstract:
    A new modelling notation and a verification tool for hybrid systems is introduced: The Cottbus Timed Automaton (CTA). In contrast to existing modelling concepts, the new formalism has the advantage to be capable of modelling hybrid systems as a modular structure of components which communicate through the elements of an explicitly defined interface. The interface consists of signals and variables declared with different access modes. This paper describes how to model a system and how to verify it. The current version of the tool using the double description method to represent the regions is presented.
    Annotation:
    FSCBS 2000, Edinburgh, April 6-7
    Charles Rattray, Miroslav Sveda, editors

    @InProceedings{FSCBS00,
    author = {Dirk Beyer and Heinrich Rust},
    title = {Modular Modelling and Verification with {C}ottbus {T}imed {A}utomata},
    booktitle = {Proceedings of the IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems (FSCBS~2000, Edinburgh, April 6-7)},
    year = {2000},
    pages = {17-24},
    address = {Stirling},
    editor = {C.~Rattray and M.~Sveda},
    isbn = {},
    keyword = {Formal Verification of Real-Time Systems},
    abstract = { A new modelling notation and a verification tool for hybrid systems is introduced: The Cottbus Timed Automaton (CTA). In contrast to existing modelling concepts, the new formalism has the advantage to be capable of modelling hybrid systems as a modular structure of components which communicate through the elements of an explicitly defined interface. The interface consists of signals and variables declared with different access modes. This paper describes how to model a system and how to verify it. The current version of the tool using the double description method to represent the regions is presented. },
    annote = {FSCBS 2000, Edinburgh, April 6-7 
    Charles Rattray, Miroslav Sveda, editors}, }

Internal reports

  1. Dirk Beyer, Claus Lewerentz, and Frank Simon. Flattening Inheritance Structures -- OR -- Getting the Right Picture of Large OO-Systems. Technical report I-12/2000, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, November 2000. [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    Abstract:
    More and more software systems are developed using the object oriented paradigm. Thus, large systems contain inheritance structures to provide a flexible and re-usable design and to allow for polymorphic method calls. This paper gives a detailed overview about the impact of using inheritance on measuring, understanding and using subclasses in such class systems. Usually, considering classes within an inheritance relation is reduced to the consideration of locally defined members of a class. This view might be incomplete or even misleading in some use cases. To provide an additional view on a given system we define a tool-supported flattening process which transforms an inheritance structure to a representation in which all the inherited members are explicit in each subclass. This representation provides additional insights for measuring, understanding, and developing large software systems.

    @TechReport{TR12-BTU00,
    author = {Dirk Beyer and Claus Lewerentz and Frank Simon},
    title = {Flattening Inheritance Structures -- OR -- {G}etting the Right Picture of Large {OO}-Systems},
    institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus},
    month = {November},
    year = {2000},
    number = {I-12/2000},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2000-BTU-TR12.Flattening_Inheritance_Structures.pdf},
    abstract = { More and more software systems are developed using the object oriented paradigm. Thus, large systems contain inheritance structures to provide a flexible and re-usable design and to allow for polymorphic method calls. This paper gives a detailed overview about the impact of using inheritance on measuring, understanding and using subclasses in such class systems. Usually, considering classes within an inheritance relation is reduced to the consideration of locally defined members of a class. This view might be incomplete or even misleading in some use cases. To provide an additional view on a given system we define a tool-supported flattening process which transforms an inheritance structure to a representation in which all the inherited members are explicit in each subclass. This representation provides additional insights for measuring, understanding, and developing large software systems. },
    
    }
    

  2. Dirk Beyer and Andreas Noack. Efficient Verification of Real-Time Systems using BDDs. Technical report I-13/2000, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, December 2000. Keyword(s): Formal Verification of Real-Time Systems.
    Annotation:
    See FMICS01 [18] for proceedings version.

    @TechReport{TR13-BTU00,
    author = {Dirk Beyer and Andreas Noack},
    title = {Efficient Verification of Real-Time Systems using {BDD}s},
    institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus},
    month = {December},
    year = {2000},
    number = {I-13/2000},
    keyword = {Formal Verification of Real-Time Systems},
    annote = {See FMICS01 [18] for proceedings version.},
    
    }
    

  3. Frank Simon and Dirk Beyer. Considering Inheritance, Overriding, Overloading and Polymorphism for Measuring C++ Sources. Technical report I-04/2000, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, May 2000. Keyword(s): Structural Analysis and Comprehension.
    Annotation:
    See IWSM00 [12] for proceedings version.

    @TechReport{TR04-BTU00,
    author = {Frank Simon and Dirk Beyer},
    title = {Considering Inheritance, Overriding, Overloading and Polymorphism for Measuring {C++} Sources},
    institution ={Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus},
    month = {May},
    year = {2000},
    number = {I-04/2000},
    keyword = {Structural Analysis and Comprehension},
    annote = {See IWSM00 [12] 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