Formal modeling of the gPTP clock synchronization algorithm in automotive ethernet

No abstract is available for this paper.

• Publication year

  2022

• Venue

  Innovations in Systems and Software Engineering

• Publication date

  2022-09-26

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/s11334-022-00483-1
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Introduction to Time-Sensitive Networking

  2022influential reference
• Time-Sensitive Networking in automotive embedded systems: State of the art and research opportunities

  2021cited by this paper
• Simulating TSN traffic scheduling and shaping for future automotive Ethernet

  2021cited by this paper
• Stuttgart, Germany

  2019cited by this paper
• Evaluation of Real-Time Ethernet with Time Synchronization and Time-Aware Shaper Using OMNeT++

  2019cited by this paper
• Time-Sensitive Networking: An Introduction

  2018influential reference
• Comparison of Time Sensitive Networking (TSN) and TTEthernet

  2018cited by this paper
• A Time-sensitive Networking (TSN) Simulation Model Based on OMNET++

  2018cited by this paper
• A Simulation Model of IEEE 802.1AS gPTP for Clock Synchronization in OMNeT++

  2018cited by this paper
• Synchronization Quality of IEEE 802.1AS in Large-Scale Industrial Automation Networks

  2017cited by this paper
• In-Vehicle Networks Outlook: Achievements and Challenges

  2016cited by this paper
• Improved clock synchronization start-up time for Ethernet AVB-based in-vehicle networks

  2015cited by this paper
• Uppaal SMC tutorial

  2015cited by this paper
• Intra-Vehicle Networks: A Review

  2015cited by this paper
• Formal Methods for Industrial Critical Systems

  2015cited by this paper
• Ethernet as an Emerging Trend in Vehicle Network Technology — Part I

  2014cited by this paper
• The TTEthernet synchronisation protocols and their formal verification

  2013cited by this paper
• Implementing a clock synchronization protocol on a multi-master Switched Ethernet network

  2013cited by this paper
• Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions

  2013cited by this paper
• Using integer clocks to verify clock-synchronization protocols

  2011cited by this paper
• Automated Formal Verification of the TTEthernet Synchronization Quality

  2011cited by this paper
• Formal verification of Time-Triggered Ethernet protocol using PRISM model checker

  2011cited by this paper
• Synchronization of audio/video bridging networks using IEEE 802.1AS

  2011cited by this paper
• SMT-Based Formal Verification of a TTEthernet Synchronization Function

  2010cited by this paper
• Model-checking Timed Temporal Logics

  2009cited by this paper
• Revisión 2.0

  2009cited by this paper
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools

  2007cited by this paper
• Modeling and Verification of a Time-triggered Networking Protocol

  2006cited by this paper
• An UPPAAL Model for Formal Verification of Master/Slave Clock Synchronization over the Controller Area Network

  2006cited by this paper
• International Conference on Networking, International Conference on Systems and International Conference on Mobile Communications and Learning Technologies (ICNICONSMCL'06)

  2006cited by this paper
• Using UPPAAL to model and verify a clock synchronization protocol for the controller area network

  2005cited by this paper
• A Tutorial on Uppaal

  2004cited by this paper
• Hardware design of a high-precision and fault-tolerant clock subsystem for CAN networks

  2003cited by this paper
• Time Triggered CAN (TTCAN)

  2001cited by this paper
• Uppaal in a nutshell

  1997cited by this paper
• Automatic verification of real-time communicating systems by constraint-solving

  1994cited by this paper
• A formally verified algorithm for clock synchronization under a hybrid fault model

  1994cited by this paper
• A Theory of Timed Automata

  1994cited by this paper
• Symbolic model checking: 1020 states and beyond

  1989cited by this paper
• Automatic verification of finite-state concurrent systems using temporal logic specifications

  1986cited by this paper
• Time, clocks, and the ordering of events in a distributed system

  1978influential reference
• Automatic Veri cation of Real-Time Communicating Systems by Constraint-Solving

  year unknowncited by this paper

• A Systematic Review on the Applications of Uppaal

  2025cites this paper
• State-of-the-art authentication and verification schemes in VANETs: A survey

  2024cites this paper
• A comprehensive survey of UPPAAL‐assisted formal modeling and verification

  2024cites this paper