@phdthesis{Beyer2002, author = {Beyer, Dirk}, title = {Formale Verifikation von Realzeit-Systemen mittels Cottbus Timed Automata}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-000000258}, school = {BTU Cottbus - Senftenberg}, year = {2002}, abstract = {Die Konstruktion eingebetteter Systeme, die starke Realzeit-Anforderungen zu erf{\"u}llen haben, wird in den verschiedensten Anwendungsbereichen immer bedeutsamer, z. B. in der Medizin, der Transporttechnik oder der Produktionsautomatisierung. Formale Methoden unterst{\"u}tzen die fehlerarme Entwicklung solcher Systeme, weil sie auf einer pr{\"a}zisen mathematischen Grundlage aufbauen. Der Autor entwickelt einen geeigneten Modellierungsformalismus und effiziente Verifikationsverfahren f{\"u}r den Einsatz einer formalen Methode. Durch die Einf{\"u}hrung eines Modulkonzepts wird die Modellierung auch großer Realzeit-Systeme systematisch unterst{\"u}tzt. F{\"u}r die Verifikation werden effiziente BDD-basierte Algorithmen verwendet, wobei auch das Problem des Findens guter BDD-Variablenordnungen gel{\"o}st wird. Es werden sowohl Erreichbarkeitsanalyse als auch Verfeinerungsanalyse unterst{\"u}tzt. Die Praktikabilit{\"a}t der Ans{\"a}tze zur Modellierung und Verifikation werden in verschiedenen Fallstudien aus den Bereichen der reaktiven Systeme und der Kommunikationsprotokolle demonstriert.}, subject = {Verteiltes System; Verifikation}, language = {de} }