Spezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAAL

dc.contributor.authorKresic, Dario
dc.contributor.authorHielscher, Kai-Steffen
dc.contributor.authorGerman, Reinhard
dc.date.accessioned2011-02-18
dc.date.available2023-10-16T13:57:59Z
dc.date.created2010
dc.date.issued2011-02-18
dc.description.abstractIn dieser Arbeit stellen wir eine durch Zeitautomaten modellierte Spezifikation des Mediumzugriffs im CAN-Protokoll vor sowie ihre Implementierung in UPPAAL. Zeitliche Anforderungen wurden dabei durch entsprechende Uhren-Nebenbedingungen erfasst. Dieses Zeitautomaten-Modell wurde anschließend automatisch verifiziert (Model Checking), wobei mehrere Anforderungen identifiziert wurden, die das CAN Protokoll erfüllen muß (wie Deadlock-Freiheit des Modells, Übertragungsrecht für die höchstpriore Nachricht, exklusives Übertragungsrecht für beliebigen CAN-Adapter nach der gewonnenen Arbitrage etc.). All diese Eigenschaften wurden in einer Variante der temporalen Logik CTL spezifiziert; die automatische Verifikation selbst wurde dabei mit UPPAAL durchgeführt, einem Model Checker für zeitautomaten-basierte Modelle.de
dc.identifier.opus-id1620
dc.identifier.urihttps://open.fau.de/handle/openfau/1620
dc.identifier.urnurn:nbn:de:bvb:29-opus-23535
dc.language.isode
dc.subjectCAN-Bus
dc.subjectMedienzugriff
dc.subjectUPPAAL
dc.subjectZeitautomaten
dc.subjectCAN bus
dc.subjectmedium access
dc.subjectmodel checking
dc.subjecttimed automata
dc.subject.ddcDDC Classification::0 Informatik, Informationswissenschaft, allgemeine Werke :: 00 Informatik, Wissen, Systeme :: 004 Datenverarbeitung; Informatik
dc.titleSpecification and Implementation of CAN Arbitration in UPPAALen
dc.titleSpezifikation und Implementation des CAN-Arbitrierungsverfahrens in UPPAALde
dc.typereport
dcterms.publisherFriedrich-Alexander-Universität Erlangen-Nürnberg (FAU)
local.sendToDnbfree*
local.series.id9
local.series.nameTechnical reports / Department Informatik
local.series.numberCS-2010-05
local.subject.fakultaetTechnische Fakultät / Technische Fakultät -ohne weitere Spezifikation-
local.subject.gndModel Checking
local.subject.gndKommunikationssystem
local.subject.gndLeistungsbewertung
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
1620_Kresic_IB_Opus.pdf
Size:
990.83 KB
Format:
Adobe Portable Document Format
Description:
Faculties & Collections