Refine
Document Type
- Conference Proceeding (2)
- Doctoral Thesis (1)
- Report (1)
Language
- English (2)
- German (1)
- Multiple Languages (1)
Has Fulltext
- yes (4)
Keywords
- Apache <Programm> (1)
- CAN bus (1)
- CAN-Bus (1)
- Car2Car (1)
- Cluster Server (1)
- Computersimulation (1)
- Connected Mobility (1)
- Diskrete Simulation (1)
- FG-IVC (1)
- FGSN, Sensornetze (1)
Institute
A methodology that integrates performance measurements and simulation of computer systems is demonstrated on a web cluster system. Main contributions include a new offline time synchronization system based on exponential Filtering, efficient timestamping using the cycle counter of modern CPUs for software monitoring, flexible instrumentation of Java application servers using aspect-oriented programming, a new input modeling approach for autocorrelated data and a detailed simulation model that includes both operating system and TCP network aspects.
In 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.
14. GI/ITG KuVS Fachgespräch Sensornetze der GI/ITG Fachgruppe Kommunikation und Verteilte Systeme