Publications about Formal Verification of RealTime Systems
Books and proceedings

Formale Verifikation von RealzeitSystemen
mittels Cottbus Timed Automata.
2002.
Mensch & Buch Verlag, Berlin.
Also: Dissertation,
Brandenburgische Technische Universität Cottbus, 2002
Keyword(s): Formal Verification of RealTime Systems
PDF
Supplement
Abstract
The construction of embedded systems which have to fulfill hard realtime 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 BDDbased 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 RealzeitSystemen mittels Cottbus Timed Automata}, year = {2002}, publisher = {Mensch~\&~Buch Verlag, Berlin}, isbn = {3898204502}, url = {http://books.google.com/books?id=psEhN74boe4C&printsec=frontcover&dq=isbn:3898204502&source=gbs_summary_r&cad=0}, pdf = {https://www.sosylab.org/research/pub/2002Dissertation.Formale_Verifikation_von_RealzeitSystemen_mittels_Cottbus_Timed_Automata.pdf}, abstract = {The construction of embedded systems which have to fulfill hard realtime 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 BDDbased 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.}, annote = {BTU version: Dissertation
Summary appeared as: SoftwaretechnikTrends, Gesellschaft für Informatik, Berlin, 23(2):4, May 2003. (ISSN 07208928)
Dissertation, describes all important concepts and details of the Rabbit project in German.}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, note = {Also: Dissertation, Brandenburgische Technische Universit{\"a}t Cottbus, 2002}, urn = {urn:nbn:de:kobv:co1000000258}, }Additional Infos
BTU version: Dissertation
Summary appeared as: SoftwaretechnikTrends, Gesellschaft für Informatik, Berlin, 23(2):4, May 2003. (ISSN 07208928)
Dissertation, describes all important concepts and details of the Rabbit project in German.
Articles in conference or workshop proceedings

Can Decision Diagrams Overcome State Space Explosion
in RealTime 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 193208, 2003.
SpringerVerlag, Heidelberg.
doi:10.1007/9783540399797_13
Keyword(s): Formal Verification of RealTime 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 nontrivial state space explosion. Secondly, they show that CDDbased tools, which currently use at least exponential space for two of the protocols, will only find polynomialsize CDDs if they use better variable orders, as the BDDbased 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 RealTime 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 = {193208}, year = {2003}, series = {LNCS~2767}, publisher = {SpringerVerlag, Heidelberg}, isbn = {3540201750}, doi = {10.1007/9783540399797_13}, url = {}, pdf = {https://www.sosylab.org/research/pub/2003FORTE.Can_Decision_Diagrams_Overcome_State_Space_Explosion_in_RealTime_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 nontrivial state space explosion. Secondly, they show that CDDbased tools, which currently use at least exponential space for two of the protocols, will only find polynomialsize CDDs if they use better variable orders, as the BDDbased 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.}, 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.}, keyword = {Formal Verification of RealTime Systems}, }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. 
Rabbit: A Tool for BDDBased Verification
of RealTime Systems.
In W. A. Hunt and
F. Somenzi, editors, Proceedings of the 15th International Conference on
Computer Aided Verification (CAV 2003, Boulder, CO, July 812), LNCS 2725, pages 122125, 2003.
SpringerVerlag, Heidelberg.
doi:10.1007/9783540450696_13
Keyword(s): Formal Verification of RealTime Systems
Publisher's Version
PDF
Abstract
This paper gives a short overview of a model checking tool for realtime 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 BDDbased 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 RealTime Systems}, booktitle = {Proceedings of the 15th International Conference on Computer Aided Verification (CAV~2003, Boulder, CO, July 812)}, editor = {W.~A.~Hunt and F.~Somenzi}, pages = {122125}, year = {2003}, series = {LNCS~2725}, publisher = {SpringerVerlag, Heidelberg}, isbn = {3540405240}, doi = {10.1007/9783540450696_13}, url = {}, pdf = {https://www.sosylab.org/research/pub/2003CAV.Rabbit_A_Tool_for_BDDBased_Verification_of_RealTime_Systems.pdf}, abstract = {This paper gives a short overview of a model checking tool for realtime 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 BDDbased version of Kronos.}, annote = {Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volume=2725&spage=122
A description of the BDDbased tool's main features.}, keyword = {Formal Verification of RealTime Systems}, }Additional Infos
Online: http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volume=2725&spage=122
A description of the BDDbased tool's main features. 
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.}, annote = {Online: http://link.springer.de/link/service/series/0558/bibs/2144/21440086.htm
Decribes how the tool checks refinement via simulation relation.}, keyword = {Formal Verification of RealTime Systems}, }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.}, 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.}, keyword = {Formal Verification of RealTime Systems}, }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. 
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.}, address = {Uppsala}, annote = {}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, } 
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.}, annote = {}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, } 
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 = {}, address = {Stirling}, annote = {}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, } 
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.}, 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}, keyword = {Formal Verification of RealTime Systems}, }Additional Infos
The pdf is a revised version of the original paper.
The full formal definition and semantics of CTA. 
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
RealTime Programming (WRTP 2000, Palma, May 1719), pages 169174, 2000.
Elsevier Science, Oxford.
doi:10.1016/s14746670(17)399500
Keyword(s): Formal Verification of RealTime 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 RealTime Programming (WRTP~2000, Palma, May 1719)}, editor = {A.~Crespo and J.~Vila}, pages = {169174}, year = {2000}, publisher = {Elsevier Science, Oxford}, isbn = {0080436862}, doi = {10.1016/s14746670(17)399500}, url = {}, annote = {Also as preprint: Proc. WRTP'00, pages 181186, Valencia, 2000.
The reference for the first version of the tool using the double decription method (DDM) for hybrid systems.}, keyword = {Formal Verification of RealTime Systems}, }Additional Infos
Also as preprint: Proc. WRTP'00, pages 181186, Valencia, 2000.
The reference for the first version of the tool using the double decription method (DDM) for hybrid systems. 
BDDbasierte Verifikation von RealzeitSystemen.
In J. Grabowski and
S. Heymer, editors, Tagungsband Formale Beschreibungstechniken für
verteilte Systeme (FBT 2000, Lübeck, June 2223), pages 7989, 2000.
Shaker Verlag, Aachen.
Keyword(s): Formal Verification of RealTime 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 BDDReprä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 2223)}, editor = {J.~Grabowski and S.~Heymer}, pages = {7989}, year = {2000}, publisher = {Shaker Verlag, Aachen}, isbn = {}, pdf = {https://www.sosylab.org/research/pub/2000FBT.BDDbasierte_Verifikation_von_RealzeitSystemen.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 BDDReprä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 = {}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, } 
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
ComputerBased Systems (FSCBS 2000, Edinburgh, April 67), pages 1724, 2000.
Keyword(s): Formal Verification of RealTime 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 ComputerBased Systems (FSCBS~2000, Edinburgh, April 67)}, editor = {C.~Rattray and M.~Sveda}, pages = {1724}, 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.}, address = {Stirling}, annote = {}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, } 
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 34), pages 287303, 2000.
Keyword(s): Formal Verification of RealTime 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 34)}, editor = {S.~Gnesi and I.~Schieferdecker and A.~Rennoch}, pages = {287303}, year = {2000}, isbn = {}, pdf = {https://www.sosylab.org/research/pub/2000FMICS.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.}, address = {Berlin}, annote = {Describes a case study for modeling and analysis using the DDMbased representation.}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, }Additional Infos
Describes a case study for modeling and analysis using the DDMbased representation. 
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 1718), pages 2734, 1999.
Herbert Utz Verlag, München.
Keyword(s): Formal Verification of RealTime 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 realtime aspects of the system. We chose a problem area where we have realtime requirements, for example the throughput of the modelled production cell. So we have to use formal methods which support models of realtime 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 1718)}, editor = {K.~Spies and B.~Sch{\"a}tz}, pages = {2734}, year = {1999}, publisher = {Herbert Utz Verlag, M{\"u}nchen}, isbn = {}, pdf = {https://www.sosylab.org/research/pub/1999FBT.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.
There are many different methods to model such reactive systems. Some of these abstract from realtime aspects of the system. We chose a problem area where we have realtime requirements, for example the throughput of the modelled production cell. So we have to use formal methods which support models of realtime systems.}, annote = {}, doinone = {DOI not available}, keyword = {Formal Verification of RealTime Systems}, } 
Modeling a Production Cell as a Distributed
RealTime 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 45), pages 148159, 1998.
Shaker Verlag, Aachen.
Keyword(s): Formal Verification of RealTime 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 CSPlike 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 RealTime System with {C}ottbus {T}imed {A}utomata}, booktitle = {Tagungsband Formale Beschreibungstechniken f{\"u}r verteilte Systeme (FBT~1998, Cottbus, June 45)}, editor = {H.~K{\"o}nig and P.~Langend{\"o}rfer}, pages = {148159}, year = {1998}, publisher = {Shaker Verlag, Aachen}, isbn = {}, pdf = {https://www.sosylab.org/research/pub/1998FBT.Modeling_a_Production_Cell_as_a_Distributed_RealTime_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 CSPlike 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.}, 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}, keyword = {Formal Verification of RealTime Systems}, }Additional Infos
The first published paper where we introduce the concepts of Cottbus Timed Automata, i.e. modules, interfaces and a modeling example.
Internal reports

A Comparative Study of Decision Diagrams
for RealTime Verification.
Technical report I03/2003, Institute of Computer Science,
Brandenburgische Technische Universität Cottbus, January 2003.
Keyword(s): Formal Verification of RealTime Systems
BibTeX Entry
@techreport{TR03BTU03, author = {Dirk Beyer and Andreas Noack}, title = {A Comparative Study of Decision Diagrams for RealTime Verification}, number = {I03/2003}, year = {2003}, annote = {See FORTE03 [26] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, keyword = {Formal Verification of RealTime Systems}, month = {January}, }Additional Infos
See FORTE03 [26] for proceedings version. 
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}, annote = {See CAV03 [25] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, keyword = {Formal Verification of RealTime Systems}, 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}, annote = {See CHARME01 [20] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, keyword = {Formal Verification of RealTime Systems}, month = {February}, }Additional Infos
See CHARME01 [20] for proceedings version. 
Efficient Verification of RealTime Systems using BDDs.
Technical report I13/2000, Institute of Computer Science,
Brandenburgische Technische Universität Cottbus, December 2000.
Keyword(s): Formal Verification of RealTime Systems
BibTeX Entry
@techreport{TR13BTU00, author = {Dirk Beyer and Andreas Noack}, title = {Efficient Verification of RealTime Systems using {BDD}s}, number = {I13/2000}, year = {2000}, annote = {See FMICS01 [18] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, keyword = {Formal Verification of RealTime Systems}, month = {December}, }Additional Infos
See FMICS01 [18] for proceedings version. 
A Formalism for Modular Modelling of Hybrid Systems.
Technical report I10/1999, Institute of Computer Science,
Brandenburgische Technische Universität Cottbus, October 1999.
Keyword(s): Formal Verification of RealTime Systems
BibTeX Entry
@techreport{TR10BTU99, author = {Dirk Beyer and Heinrich Rust}, title = {A Formalism for Modular Modelling of Hybrid Systems}, number = {I10/1999}, year = {1999}, annote = {See FSCBS01 [16] for proceedings version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, keyword = {Formal Verification of RealTime Systems}, month = {October}, }Additional Infos
See FSCBS01 [16] for proceedings version. 
A Modular Hybrid Modelling Notation.
Technical report I03/1999, Institute of Computer Science,
Brandenburgische Technische Universität Cottbus, February 1999.
Keyword(s): Formal Verification of RealTime Systems
BibTeX Entry
@techreport{TR03BTU99, author = {Dirk Beyer and Heinrich Rust}, title = {A Modular Hybrid Modelling Notation}, number = {I03/1999}, year = {1999}, annote = {See TR10BTU99 [04] for revised version.}, institution = {Institute of Computer Science, Brandenburgische Technische Universit{\"a}t Cottbus}, keyword = {Formal Verification of RealTime Systems}, month = {February}, }Additional Infos
See TR10BTU99 [04] for revised version.
Theses and projects (PhD, MSc, BSc, Project)

BDDbasierte Verifikation von Echtzeitsystemen.
Master's Thesis, BTU Cottbus, with Prof. Claus Lewerentz, 2000.
Keyword(s): Formal Verification of RealTime Systems
BibTeX Entry
@misc{NoackBDD, author = {Andreas Noack}, title = {{BDDbasierte Verifikation von Echtzeitsystemen}}, year = {2000}, pdf = {}, annote = {Won the BTU University Award 2000 for best Master’s thesis}, howpublished = {Master's Thesis, BTU Cottbus, with Prof. Claus Lewerentz}, keyword = {Formal Verification of RealTime Systems}, }Additional Infos
Won the BTU University Award 2000 for best Master’s thesis 
Rabbit: Verification of RealTime Systems.
1998.
Keyword(s): Software Development Project,
Formal Verification of RealTime Systems
Supplement
BibTeX Entry
@misc{Rabbit, title = {{{\sc Rabbit}}: Verification of RealTime Systems}, year = {1998}, url = {http://www.sosylab.org/~dbeyer/Rabbit/}, keyword = {Software Development Project,Formal Verification of RealTime Systems}, role = {Principal designer and implementer}, }
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.