Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Innovations in Systems and Software Engineering
Published 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

Authors: Shimmi Asokan, G. Santhosh Kumar

Published in: Innovations in Systems and Software Engineering | Issue 3/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article Efficiency of oversampling methods for enhancing software defect prediction by using imbalanced data
next article Frequent itemset mining using FP-tree: a CLA-based approach and its extended application in biodiversity data

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Literature
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.
Metadata
Title
Formal modeling of the gPTP clock synchronization algorithm in automotive ethernet
Authors
Shimmi Asokan
G. Santhosh Kumar
Publication date
26-09-2022
Publisher
Springer London
Published in
Innovations in Systems and Software Engineering / Issue 3/2023
Print ISSN: 1614-5046
Electronic ISSN: 1614-5054
DOI
https://doi.org/10.1007/s11334-022-00483-1

Other articles of this Issue 3/2023

Innovations in Systems and Software Engineering 3/2023 Go to the issue

Original Article

Component level diagnosability of discrete event systems based on observations

Original Article

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

Review Article

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

Original Article

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

Original Article

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

Premium Partner

    Image Credits