Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Innovations in Systems and Software Engineering
Erschienen in: Innovations in Systems and Software Engineering 3/2023

26.09.2022 | Original Article

Formal modeling of the gPTP clock synchronization algorithm in automotive ethernet

verfasst von: Shimmi Asokan, G. Santhosh Kumar

Erschienen in: Innovations in Systems and Software Engineering | Ausgabe 3/2023

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Major manufacturers in the automotive industry are now adopting automotive Ethernet as the In-Vehicle Network standard. The increased bandwidth and lower cost have been the motivating factors to use automotive Ethernet as the backbone for interconnecting various components within the vehicle. The components that control the critical functions in the vehicle should have a synchronized time base. IEEE 802.1 AS-Rev, the specification for timing and synchronization employs generalized Precision Time Protocol (gPTP) for clock synchronization in automotive Ethernet. In a network of time-aware systems, gPTP imposes that, the clocks of all the nodes in the network have to be synchronized to the clock of the Grand Master for flawless communication in the network. The paper proposes a formal model of the gPTP protocol using UPPAAL model checker. This enables us to formally verify the protocol for its properties. The communication between the master and the slave nodes were modeled and it is verified that the divergence between the master clock and the slave clock is always within the precision.
Vorheriger Artikel Efficiency of oversampling methods for enhancing software defect prediction by using imbalanced data
Nächster Artikel Frequent itemset mining using FP-tree: a CLA-based approach and its extended application in biodiversity data

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Literatur
1.
Zeng W, Khalid MA, Chowdhury S (2016) In-vehicle networks outlook: achievements and challenges. IEEE Commun Surv Tutor 18(3):1552–1571CrossRef
2.
Tuohy S, Glavin M, Hughes C, Jones E, Trivedi M, Kilmartin L (2014) Intra-vehicle networks: a review. IEEE Trans Intell Transp Syst 16(2):534–545CrossRef
3.
Specification CAN (1991) Robert Bosch GmbH. Stuttgart, Germany
4.
Package, LIN Specification, (2003) Revision 2.0. LIN consortium
5.
FlexRay Consortium J (2005) FlexRay communications system protocol specification version 2.1
6.
Cooperation MOST (2004) MOST Media Oriented Systems Transport specification, version 2.3
7.
Ashjaei M, Bello LL, Daneshtalab M, Patti G, Saponara S, Mubeen S (2021) Time-Sensitive Networking in automotive embedded systems: state of the art and research opportunities. J Syst Architect 117:102137CrossRef
8.
Prasad M, Dey RK, Sardar A, Goswami G (2014) Ethernet as an emerging trend in vehicle network technology—part I. Auto Tech Rev 3(12):18–23CrossRef
9.
Prasad M, Dey RK, Sardar A (2015) Ethernet as an emerging trend in vehicle network technology—part II. Auto Tech Rev 4:18–23CrossRef
10.
Zhao L, He F, Li E, Lu J (2018) Comparison of time sensitive networking (TSN) and TT Ethernet. In 2018 IEEE/AIAA 37th digital avionics systems conference (DASC). IEEE, pp 1–7
11.
Messenger JL (2018) Time-sensitive networking: an introduction. IEEE Commun Stand Mag 2(2):29–33CrossRef
12.
Finn N (2018) Introduction to time-sensitive networking. IEEE Commun Stand Mag 2(2):22–28CrossRef
13.
Fuehrer T, Mueller B, Hartwich F, Hugel R (2001) Time triggered CAN (ttcan). SAE transactions, pp 143–149
14.
Le C, Qiao D (2019) Evaluation of real-time ethernet with time synchronization and time-aware shaper using OMNeT++. In: 2019 IEEE 2nd international conference on electronics technology (ICET). IEEE, pp 70–73
15.
Zhou Z, Lee J, Berger MS, Park S, Yan Y (2021) Simulating TSN traffic scheduling and shaping for future automotive Ethernet. J Commun Netw 23(1):53–62CrossRef
16.
IEEE Standards Association (2011) IEEE Standard for Local and Metropolitan Area Networks-Timing and Synchronization for Time-Sensitive Applications in Bridged Local Area Networks. IEEE Std, 802. 1AS-2011
17.
IEEE Standards Association (2019) IEEE Standard for Local and Metropolitan Area Networks-Timing and Synchronization for Time-Sensitive Applications-IEEE Std 802.1AS-Rev, Draft 8.0
18.
IEEE Standards Association (2008) IEEE Standard 1588-2008 (Revision of IEEE Std 1588-2002), IEEE Standard for a Precision Clock Synchronization Protocol for Networked Measurement and Control Systems
19.
Puttnies H, Danielis P, Janchivnyambuu E, Timmermann D (2018) A simulation model of IEEE 802.1 AS gPTP for clock synchronization in OMNeT++. In OMNeT++. EPiC Ser Comput 56:63–72
20.
Jiang J, Li Y, Hong SH, Xu A, Wang K (2018, August) A time-sensitive networking (TSN) simulation model based on OMNET++. In: 2018 IEEE international conference on mechatronics and automation (ICMA). IEEE, pp 643–648
21.
Behrmann G, David A, Larsen KG (2004) A tutorial on UPPAAL. In: Bernardo M, Corradini F (eds) SFM-RT 2004. LNCS, vol. 3185. Springer, Heidelberg, pp. 200–236
22.
Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1):134–152CrossRefMATH
23.
David A, Larsen KG, Legay A, Mikučionis M, Poulsen DB (2015) Uppaal SMC tutorial. Int J Softw Tools Technol Transf 17(4):397–415CrossRef
24.
Lamport L (1978) Time, clocks, and the ordering of events in a distributed system, the Ordering of Events in a Distributed System. Commun ACM 21(7):558–565CrossRefMATH
25.
Rushby J (1994) A formally verified algorithm for clock synchronization under a hybrid fault model. In: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, pp 304–313
26.
Rodriguez-Navas G, Proenza J (2012) Using timed automata for modeling distributed systems with clocks: challenges and solutions. IEEE Trans Softw Eng 39(6):857–868CrossRef
27.
Barsotti D, Nieto LP, Tiu A (2007) Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Formal Aspects Comput 19(3):321–341CrossRefMATH
28.
Rodríguez-Navas G, Bosch JJ, Proenza J (2003) Hardware design of a high-precision and fault-tolerant clock subsystem for CAN networks. IFAC Proc Vol 36(13):39–46CrossRef
29.
Rodriguez-Navas G, Proenza J, Hansson H (2005) Using UPPAAL to model and verify a clock synchronization protocol for the controller area network. In: 2005 IEEE conference on emerging technologies and factory automation. IEEE, vol 2
30.
Rodriguez-Navas G, Proenza J, Hansson H (2006) An UPPAAL model for formal verification of master/slave clock synchronization over the controller area network. In: Proceedings of the 6th IEEE international workshop on factory communication systems, Torino, Italy. IEEE Computer Society Press, Los Alamitos
31.
Leen G, Heffernan D (2006) Modeling and verification of a time-triggered networking protocol. In: International conference on networking, international conference on systems and international conference on mobile communications and learning technologies (ICNICONSMCL’06). IEEE, pp 178–178
32.
Leen G, Heffernan D (2002) Formally Verifying Aspects of Time-Triggered Controller Area Network (Phases 1 & 2a). Tech. report, PEI/CSRC report no. 20020603, main library, University of Limerick
33.
Steiner W, Dutertre B (2010) SMT-Based formal verification of a TT Ethernet synchronization function. In: International workshop on formal methods for industrial critical systems. Springer, Berlin, Heidelberg, pp 148–163
34.
Steiner W, Dutertre B (2011) Automated formal verification of the TT Ethernet synchronization quality. In: NASA formal methods symposium. Springer, Berlin, Heidelberg, pp 375–390
35.
Steiner W, Dutertre B (2013) The TT Ethernet synchronisation protocols and their formal verification. Int J Crit Comput Based Syst 174(3):280–300CrossRef
36.
Ammar M, Mohamed OA (2011) Formal verification of Time-Triggered Ethernet protocol using PRISM model checker. In: Proceedings of ICM 2011. IEEE, pp 1–5
37.
38.
Ashjaei M, Behnam M, Rodriguez-Navas G, Nolte T (2013) Implementing a clock synchronization protocol on a multi-master switched ethernet network. In: 2013 IEEE 18th conference on emerging technologies & factory automation (ETFA). IEEE, pp 1–10
39.
Gutiérrez M, Steiner W, Dobrin R, Punnekkat S (2017) Synchronization quality of IEEE 802.1 AS in large-scale industrial automation networks. In: 2017 IEEE real-time and embedded technology and applications symposium (RTAS). IEEE, pp 273–282
40.
Garner GM, Ryu H (2011) Synchronization of audio/video bridging networks using IEEE 802.1 AS. IEEE Commun Mag 49(2):140–147CrossRef
41.
Diarra A, Hogenmueller T, Zimmermann A, Grzemba A, Khan UA (2015) Improved clock synchronization start-up time for Ethernet AVB-based in-vehicle networks. In: 2015 IEEE 20th conference on emerging technologies & factory automation (ETFA). IEEE, pp 1–8
42.
43.
Yi W, Pettersson P, Daniels M (1995) Automatic verification of real-time communicating systems by constraint-solving. In: Formal description techniques VII. Springer, Boston, MA, pp 243–258
44.
45.
Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst (TOPLAS) 8(2):244–263CrossRefMATH
46.
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170CrossRefMATH
47.
Huang X, Singh A, Smolka SA (2011) Using integer clocks to verify clock-synchronization protocols. Innov Syst Softw Eng 7(2):119–130CrossRef
48.
Metadaten
Titel
Formal modeling of the gPTP clock synchronization algorithm in automotive ethernet
verfasst von
Shimmi Asokan
G. Santhosh Kumar
Publikationsdatum
26.09.2022
Verlag
Springer London
Erschienen in
Innovations in Systems and Software Engineering / Ausgabe 3/2023
Print ISSN: 1614-5046
Elektronische ISSN: 1614-5054
DOI
https://doi.org/10.1007/s11334-022-00483-1

Weitere Artikel der Ausgabe 3/2023

Innovations in Systems and Software Engineering 3/2023 Zur Ausgabe

Original Article

Efficiency of oversampling methods for enhancing software defect prediction by using imbalanced data

Original Article

Component level diagnosability of discrete event systems based on observations

Review Article

An improved authentication and key management scheme for hierarchical IoT network using elliptic curve cryptography

Original Article

Frequent itemset mining using FP-tree: a CLA-based approach and its extended application in biodiversity data

Original Article

TimeLine Depiction: an approach to graphical notation for supporting temporal property specification

Premium Partner

    Bildnachweise