Software and Computational Systems Lab

Publications about Formal Verification of Real-Time Systems

1. Dirk Beyer. Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata. 2002. Mensch & Buch Verlag, Berlin. Also: Dissertation, Brandenburgische Technische Universität Cottbus, 2002 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF Supplement
   Abstract

   The construction of embedded systems which have to fulfill hard real-time requirements is becoming more and more important in various application areas, e. g. in medicine, in transport technology, or in production automation. Formal methods support the development of faultless systems because they use a precise mathematical basis. The author developed a suitable modelling formalism and efficient verification methods to enable the application of a formal method. Due to the module concept introduced in the thesis, the modelling of large systems is supported systematically. For the verification efficient BDD-based algorithms are used, and the problem of finding good BDD variable orderings is solved. Reachability analysis as well as refinement checking are provided. The practicability of the approaches for modelling and verification is demonstrated by presenting various case studies from the application areas of reactive systems and protocol engineering.
   BibTeX Entry

   @book{Diss02, author = {Dirk Beyer}, title = {Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata}, year = {2002}, publisher = {Mensch~\&~Buch Verlag, Berlin}, isbn = {3-89820-450-2}, url = {http://books.google.com/books?id=psEhN74boe4C&printsec=frontcover&dq=isbn:3898204502&source=gbs_summary_r&cad=0}, pdf = {https://www.sosy-lab.org/research/pub/2002-Dissertation.Formale_Verifikation_von_Realzeit-Systemen_mittels_Cottbus_Timed_Automata.pdf}, abstract = {The construction of embedded systems which have to fulfill hard real-time requirements is becoming more and more important in various application areas, e. g. in medicine, in transport technology, or in production automation. Formal methods support the development of faultless systems because they use a precise mathematical basis. The author developed a suitable modelling formalism and efficient verification methods to enable the application of a formal method. Due to the module concept introduced in the thesis, the modelling of large systems is supported systematically. For the verification efficient BDD-based algorithms are used, and the problem of finding good BDD variable orderings is solved. Reachability analysis as well as refinement checking are provided. The practicability of the approaches for modelling and verification is demonstrated by presenting various case studies from the application areas of reactive systems and protocol engineering.}, keyword = {Formal Verification of Real-Time Systems}, annote = {BTU version: <a href="https://www.sosy-lab.org/research/pub/2002-Dissertation.Formale_Verifikation_von_Realzeit-Systemen_mittels_Cottbus_Timed_Automata.BTU.pdf"> <img align="middle" border="0" src="../../pub/Icons/pdf.gif"> Dissertation</a> <BR> Summary appeared as: Softwaretechnik-Trends, Gesellschaft f&uuml;r Informatik, Berlin, 23(2):4, May 2003. (ISSN 0720-8928) <BR> Dissertation, describes all important concepts and details of the Rabbit project in German.}, doinone = {DOI not available}, note = {Also: Dissertation, Brandenburgische Technische Universit{\"a}t Cottbus, 2002}, urn = {urn:nbn:de:kobv:co1-000000258}, }
   Additional Infos

   BTU version: Dissertation
   Summary appeared as: Softwaretechnik-Trends, Gesellschaft für Informatik, Berlin, 23(2):4, May 2003. (ISSN 0720-8928)
   Dissertation, describes all important concepts and details of the Rabbit project in German.

2. Dirk Beyer and Andreas Noack. Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?. In H. König, M. Heiner, and A. Wolisz, editors, Proceedings of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2003, Berlin, September 29 - October 2), LNCS 2767, pages 193-208, 2003. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-39979-7_13 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF
   Abstract

   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.
   BibTeX Entry

   @inproceedings{FORTE03, author = {Dirk Beyer and Andreas Noack}, title = {Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?}, booktitle = {Proceedings of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (FORTE~2003, Berlin, September 29 - October 2)}, editor = {H.~K{\"o}nig and M.~Heiner and A.~Wolisz}, pages = {193-208}, year = {2003}, series = {LNCS~2767}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-20175-0}, doi = {10.1007/978-3-540-39979-7_13}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2003-FORTE.Can_Decision_Diagrams_Overcome_State_Space_Explosion_in_Real-Time_Verification.pdf}, abstract = {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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {Analysis of the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Analytical and empirical complexity results for three communication protocols.}, }
   Additional Infos

   Analysis of the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Analytical and empirical complexity results for three communication protocols.
3. Dirk Beyer, Claus Lewerentz, and Andreas Noack. Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. In W. A. Hunt and F. Somenzi, editors, Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003, Boulder, CO, July 8-12), LNCS 2725, pages 122-125, 2003. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-45069-6_13 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF
   Abstract

   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.
   BibTeX Entry

   @inproceedings{CAV03, author = {Dirk Beyer and Claus Lewerentz and Andreas Noack}, title = {Rabbit: A Tool for {BDD}-Based Verification of Real-Time Systems}, booktitle = {Proceedings of the 15th International Conference on Computer Aided Verification (CAV~2003, Boulder, CO, July 8-12)}, editor = {W.~A.~Hunt and F.~Somenzi}, pages = {122-125}, year = {2003}, series = {LNCS~2725}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-40524-0}, doi = {10.1007/978-3-540-45069-6_13}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2003-CAV.Rabbit_A_Tool_for_BDD-Based_Verification_of_Real-Time_Systems.pdf}, abstract = {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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {Online: <a href="http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122"> http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122</a> <BR> A description of the BDD-based tool's main features.}, }
   Additional Infos

   Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2725&spage=122
   A description of the BDD-based tool's main features.
4. 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. doi:10.1007/3-540-44798-9_6 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version PDF
   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.
   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 4-7)}, editor = {T.~Margaria and T.~F.~Melham}, pages = {86-91}, year = {2001}, series = {LNCS~2144}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-42541-1}, doi = {10.1007/3-540-44798-9_6}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2001-CHARME.Efficient_Reachability_Analysis_and_Refinement_Checking_of_Timed_Automata_using_BDDs.pdf}, 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {Online: <a href="http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm"> http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm</a> <BR> 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.
5. 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. doi:10.1007/3-540-45251-6_18 Keyword(s): Formal Verification of Real-Time 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 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.
   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 12-16): Formal Methods for Increasing Software Productivity}, editor = {J.~N.~Oliveira and P.~Zave}, pages = {318-343}, year = {2001}, series = {LNCS~2021}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-41791-5}, doi = {10.1007/3-540-45251-6_18}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2001-FME.Improvements_in_BDD-Based_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 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {Online: <a href="http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm"> http://link.springer.de/link/service/series/0558/bibs/2021/20210318.htm</a> <BR> 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.}, }
   Additional Infos

   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.
6. 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), pages 13-21, 2001. Keyword(s): Formal 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.
   BibTeX Entry

   @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}, year = {2001}, isbn = {}, 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.}, keyword = {Formal Verification of Real-Time Systems}, address = {Uppsala}, annote = {}, doinone = {DOI not available}, }
7. 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. Keyword(s): Formal Verification of Real-Time 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 on-the-fly 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 16-17)}, editor = {S.~Gnesi and U.~Ultes-Nitsche}, pages = {95-113}, year = {2001}, publisher = {INRIA, Paris}, isbn = {}, 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {}, doinone = {DOI not available}, }
8. 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), pages 89-98, 2001. Keyword(s): Formal Verification of Real-Time 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 Computer-Based Systems (FSCBS~2001, Washington, D.C., April 20)}, editor = {C.~Rattray and M.~Sveda and J.~Rozenblit}, pages = {89-98}, year = {2001}, isbn = {}, keyword = {Formal Verification of Real-Time Systems}, address = {Stirling}, annote = {}, doinone = {DOI not available}, }
9. 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), pages 75-87, 2001. Keyword(s): Formal Verification of Real-Time 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 write-access 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 Computer-Based Systems (FSCBS~2001, Washington, D.C., April 20)}, editor = {C.~Rattray and M.~Sveda and J.~Rozenblit}, pages = {75-87}, year = {2001}, isbn = {}, 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.}, keyword = {Formal Verification of Real-Time Systems}, address = {Stirling}, annote = {The pdf is a revised version of the original paper. <BR> 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.
10. 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. doi:10.1016/s1474-6670(17)39950-0 Keyword(s): Formal Verification of Real-Time Systems Publisher's Version
    BibTeX Entry

    @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)}, editor = {A.~Crespo and J.~Vila}, pages = {169-174}, year = {2000}, publisher = {Elsevier Science, Oxford}, isbn = {0-08-043686-2}, doi = {10.1016/s1474-6670(17)39950-0}, url = {}, keyword = {Formal Verification of Real-Time Systems}, annote = {Also as preprint: Proc. WRTP'00, pages 181-186, Valencia, 2000. <BR> The reference for the first version of the tool using the double decription method (DDM) for hybrid systems.}, }
    Additional Infos

    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.
11. 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. Keyword(s): Formal Verification of Real-Time Systems 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.
    BibTeX Entry

    @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 = {}, 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.}, keyword = {Formal Verification of Real-Time Systems}, annote = {}, doinone = {DOI not available}, }
12. 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), 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.
    BibTeX Entry

    @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)}, editor = {C.~Rattray and M.~Sveda}, pages = {17-24}, year = {2000}, isbn = {}, 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.}, keyword = {Formal Verification of Real-Time Systems}, address = {Stirling}, annote = {}, doinone = {DOI not available}, }
13. 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), pages 287-303, 2000. Keyword(s): Formal Verification of Real-Time Systems 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.
    BibTeX Entry

    @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}, pages = {287-303}, year = {2000}, isbn = {}, 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.}, keyword = {Formal Verification of Real-Time Systems}, address = {Berlin}, annote = {Describes a case study for modeling and analysis using the DDM-based representation.}, doinone = {DOI not available}, }
    Additional Infos

    Describes a case study for modeling and analysis using the DDM-based representation.
14. Dirk Beyer and Heinrich Rust. Concepts of Cottbus Timed Automata. In K. Spies and B. Schätz, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT 1999, München, June 17-18), pages 27-34, 1999. Herbert Utz Verlag, München. Keyword(s): Formal Verification of Real-Time Systems PDF
    Abstract

    Today, many industrial production cells are controlled by software. Many such systems have to deal with requirements which the developer has to guarantee. Because of the complexity of the implementation one of the main problems for developing the software for reactive systems is to be sure that such properties are fulfilled. One way to handle the problems is to use formal methods: This means to develop a formal model which is used to prove the properties of the specification with tool support.
    There are many different methods to model such reactive systems. Some of these abstract from real-time aspects of the system. We chose a problem area where we have real-time requirements, for example the throughput of the modelled production cell. So we have to use formal methods which support models of real-time systems.
    BibTeX Entry

    @inproceedings{FBT99, author = {Dirk Beyer and Heinrich Rust}, title = {Concepts of {C}ottbus {T}imed {A}utomata}, booktitle = {Tagungsband Formale Beschreibungstechniken f{\"u}r verteilte Systeme (FBT~1999, M{\"u}nchen, June 17-18)}, editor = {K.~Spies and B.~Sch{\"a}tz}, pages = {27-34}, year = {1999}, publisher = {Herbert Utz Verlag, M{\"u}nchen}, isbn = {}, pdf = {https://www.sosy-lab.org/research/pub/1999-FBT.Concepts_of_Cottbus_Timed_Automata.pdf}, abstract = {Today, many industrial production cells are controlled by software. Many such systems have to deal with requirements which the developer has to guarantee. Because of the complexity of the implementation one of the main problems for developing the software for reactive systems is to be sure that such properties are fulfilled. One way to handle the problems is to use formal methods: This means to develop a formal model which is used to prove the properties of the specification with tool support. <BR> There are many different methods to model such reactive systems. Some of these abstract from real-time aspects of the system. We chose a problem area where we have real-time requirements, for example the throughput of the modelled production cell. So we have to use formal methods which support models of real-time systems.}, keyword = {Formal Verification of Real-Time Systems}, annote = {}, doinone = {DOI not available}, }
15. Dirk Beyer and Heinrich Rust. Modeling a Production Cell as a Distributed Real-Time System with Cottbus Timed Automata. In H. König and P. Langendörfer, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT 1998, Cottbus, June 4-5), pages 148-159, 1998. Shaker Verlag, Aachen. Keyword(s): Formal Verification of Real-Time Systems PDF
    Abstract

    We build on work in designing modeling languages for hybrid systems in the development of CTA, the Cottbus Timed Automata. Our design features a facility to specify a hybrid system modulary and hierarchically, communication through CSP-like synchronizations but with special support to specify explicitly different roles which the interface signals and variables of a module play, and to instantiate recurring elements serveral times from a template. Continuous system components are modeled with analogue variables having piecewise constant derivatives. Discrete system aspects like control modes are modeled with the discrete variables and the states of a finite automaton. Our approach to specifying distributed hybrid systems is illustrated with the specification of a component of a production cell, a transport belt.
    BibTeX Entry

    @inproceedings{FBT98, author = {Dirk Beyer and Heinrich Rust}, title = {Modeling a Production Cell as a Distributed Real-Time System with {C}ottbus {T}imed {A}utomata}, booktitle = {Tagungsband Formale Beschreibungstechniken f{\"u}r verteilte Systeme (FBT~1998, Cottbus, June 4-5)}, editor = {H.~K{\"o}nig and P.~Langend{\"o}rfer}, pages = {148-159}, year = {1998}, publisher = {Shaker Verlag, Aachen}, isbn = {}, pdf = {https://www.sosy-lab.org/research/pub/1998-FBT.Modeling_a_Production_Cell_as_a_Distributed_Real-Time_System_with.Cottbus_Timed_Automata.pdf}, abstract = {We build on work in designing modeling languages for hybrid systems in the development of CTA, the Cottbus Timed Automata. Our design features a facility to specify a hybrid system modulary and hierarchically, communication through CSP-like synchronizations but with special support to specify explicitly different roles which the interface signals and variables of a module play, and to instantiate recurring elements serveral times from a template. Continuous system components are modeled with analogue variables having piecewise constant derivatives. Discrete system aspects like control modes are modeled with the discrete variables and the states of a finite automaton. Our approach to specifying distributed hybrid systems is illustrated with the specification of a component of a production cell, a transport belt.}, keyword = {Formal Verification of Real-Time Systems}, annote = {The first published paper where we introduce the concepts of Cottbus Timed Automata, i.e. modules, interfaces and a modeling example.}, doinone = {DOI not available}, }
    Additional Infos

    The first published paper where we introduce the concepts of Cottbus Timed Automata, i.e. modules, interfaces and a modeling example.

16. Dirk Beyer and Andreas Noack. A Comparative Study of Decision Diagrams for Real-Time Verification. Technical report I-03/2003, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, January 2003. Keyword(s): Formal Verification of Real-Time Systems
    BibTeX Entry

    @techreport{TR03-BTU03, author = {Dirk Beyer and Andreas Noack}, title = {A Comparative Study of Decision Diagrams for Real-Time Verification}, number = {I-03/2003}, year = {2003}, keyword = {Formal Verification of Real-Time Systems}, annote = {See FORTE03 [26] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {January}, }
    Additional Infos

    See FORTE03 [26] for proceedings version.
17. 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
    BibTeX Entry

    @techreport{TR05-BTU01, author = {Dirk Beyer}, title = {Rabbit: Verification of Real-Time Systems}, number = {I-05/2001}, year = {2001}, keyword = {Formal Verification of Real-Time 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.
18. 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
    BibTeX Entry

    @techreport{TR04-BTU01, author = {Dirk Beyer}, title = {Reachability Analysis and Refinement Checking for {BDD}-Based Model Checking of Timed Automata}, number = {I-04/2001}, year = {2001}, keyword = {Formal Verification of Real-Time 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.
19. 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
    BibTeX Entry

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

    See FMICS01 [18] for proceedings version.
20. Dirk Beyer and Heinrich Rust. A Formalism for Modular Modelling of Hybrid Systems. Technical report I-10/1999, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, October 1999. Keyword(s): Formal Verification of Real-Time Systems
    BibTeX Entry

    @techreport{TR10-BTU99, author = {Dirk Beyer and Heinrich Rust}, title = {A Formalism for Modular Modelling of Hybrid Systems}, number = {I-10/1999}, year = {1999}, keyword = {Formal Verification of Real-Time Systems}, annote = {See FSCBS01 [16] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {October}, }
    Additional Infos

    See FSCBS01 [16] for proceedings version.
21. Dirk Beyer and Heinrich Rust. A Modular Hybrid Modelling Notation. Technical report I-03/1999, Institute of Computer Science, Brandenburgische Technische Universität Cottbus, February 1999. Keyword(s): Formal Verification of Real-Time Systems
    BibTeX Entry

    @techreport{TR03-BTU99, author = {Dirk Beyer and Heinrich Rust}, title = {A Modular Hybrid Modelling Notation}, number = {I-03/1999}, year = {1999}, keyword = {Formal Verification of Real-Time Systems}, annote = {See TR10-BTU99 [04] for revised version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, month = {February}, }
    Additional Infos

    See TR10-BTU99 [04] for revised version.

22. Andreas Noack. BDD-basierte Verifikation von Echtzeitsystemen. Master's Thesis, BTU Cottbus, with Prof. Claus Lewerentz, 2000. Keyword(s): Formal Verification of Real-Time Systems
    BibTeX Entry

    @misc{NoackBDD, author = {Andreas Noack}, title = {{BDD-basierte Verifikation von Echtzeitsystemen}}, year = {2000}, pdf = {}, keyword = {Formal Verification of Real-Time Systems}, annote = {Won the BTU University Award 2000 for best Master’s thesis}, howpublished = {Master's Thesis, BTU Cottbus, with Prof. Claus Lewerentz}, }
    Additional Infos

    Won the BTU University Award 2000 for best Master’s thesis
23. Rabbit: Verification of Real-Time Systems. 1998. Keyword(s): Software Development Project, Formal Verification of Real-Time Systems Supplement
    BibTeX Entry

    @misc{Rabbit, title = {{{\sc Rabbit}}: Verification of Real-Time Systems}, year = {1998}, url = {http://www.sosy-lab.org/~dbeyer/Rabbit/}, keyword = {Software Development Project,Formal Verification of Real-Time Systems}, role = {Principal designer and implementer}, }