Notes
Outline
The Rare Glitch Project:
Verifying Bus Protocols for Embedded Systems
Edmund Clarke,  Daniel Kroening
Carnegie Mellon University
Motivation
Shorthand for Time-Triggered Protocol for SAE Class C Applications [SAE93]
Real-time communication protocol for
fault-tolerant real-time systems
Defined by draft standard TTP/C version 0.5 from TTTech AG [TTPC99]
Designed for X-by-wire applications
steer-by-wire, break-by-wire, throttle-by-wire, ...
E.g., replace steering wheel by a joystick
Safety critical!
Introduction
First used for military aircrafts (fly-by-wire)
Steer-by-Wire: replace steering wheel by joystick
Brake-by-Wire: replace hydraulic brake system
Throttle-by-Wire: replace mechanic throttle pedal
Introduction
Drive by wire
Introduction
More safety by stabilizing algorithms
Passive safety: no steering column
Reduced weight
Reduced maintenance cost
Introduction
Components are connected using a redundant bus
Introduction
Introduction
Also the smallest
replaceable unit
(SRU)
Host Processor
Protocol Processor
Bus Guardian
Line Interfaces
Introduction
TTP/C is uses a cyclic time-division multiple access (TDMA) scheme
        Time slots are assigned statically
Introduction
Daimler Chrysler / BMW tested TTP/C and considered it to be too inflexible
They developed FlexRay, which provides more flexibility
The developers of TTP/C claim that FlexRay sacrifices safety for flexibility
GM has not decided yet which protocol to use
Introduction
Large state space per node
(message area)
Many features besides message transmission (membership service, global time base, mode changes, reconfiguration, download)
Protocol provides clock synchronization
Must have large number of nodes
Verifying with only 2 or 3 nodes is dangerous, protocol requires 4 minimum, 20-30 nodes realistic
Formalizing TTP/C
The TTP/C standard is plain, informal English text
In a Drive-by-wire system, different implementations from different vendors are used
We do not verify a particular implementation
but the requirements for all implementations
Use non-determinism to cover all implementation details
Formalizing TTP/C
1.  Define set of states
Formalizing TTP/C
1.  Define set of states
Formalizing TTP/C
1.  Define set of states
Formalizing TTP/C
1.  Define set of states
Formalizing TTP/C
Abstraction...
permits concise specification of protocol properties
allows for automated, computer aided verification
Abstraction on time:
Only consider specific points of time
E.g., end of TDMA round, end of message, etc.
Formalizing TTP/C
Formalizing TTP/C
Each level is modeled by a mathematical machine
The machines share the same configuration set
The set of reachable states of a lower level is a refinement of the reachable states of a level above
Formalizing TTP/C
Formalizing TTP/C
    Let rx denote the transition relation for level x
    Let a, b denote levels and let b<a hold.
           c ra d holds
     iff   there is a set of states c1, …, cn with
           ci rb ci+1 for i=1 to n-1 and
           c1=c and cn=d
     n can be fixed depending on the level and on c1.
Verifying Protocol Properties
Service Guarantee
Verify that protocol stack can transmit messages within a finite amount of time after enabling the controller
Verify a guarantee for hot standby nodes to become member in case of a failure
Membership service
Informs all nodes about the operational state of each node within one TDMA round
SRU is operational if the host sends a life sign and the controller is operational and synchronized
Claim: membership bit matches real status after one TDMA round
Verifying Protocol Properties
Described in standard
System must tolerate any single hardware fault
System must tolerate malicious host software
  … assuming that all SRUs are implemented
  according to the standard
Verifying Protocol Properties
Uses implicit acknowledgement scheme
Encoded in CRC that protects the frames
A node that sends no or false data looses membership
After sending a frame, a node watches the following frames to determine if it is still considered a member of the cluster
Project Status
Verification done using PVS
Abstraction hierarchy
Initial predicate
Transition relation
for message slot abstraction level and abstraction levels above; for MFM code level
includes membership service
without mode changes, download, and reconfiguration
Parts of the Verification of the Membership Service
Project Status
More Properties
Analysis of Problems of Membership Service
More abstraction levels (e.g., clock synchronization)
FlexRay (requires NDA)
Prove abstraction hierarchy using theorem prover,
model-check the individual levels of the hierarchy
Common Framework: SyMP
Probabilistic Model Checking (J. Wing)
Outline
Introduction
Project Goals
Formalizing TTP/C
Verifying Protocol Properties
Project Status
Verifying Protocol Properties
No data is accepted from a node without consistent
membership information
Membership service is therefore safety critical
Problem: Correctly working nodes may loose membership
One is maybe better off without Membership Service
Verifying Protocol Properties
Nodes: A, D, E, … from Vendor 1, B, C from Vendor 2
A transmits message, correctly received by D, E… but not by B, C
A looses membership; can continue with next predecessor of B
Project Goals
Formalization of the requirements of
TTP/C and FlexRay
Formalization of service requirements of
higher levels
Formalization of a fault model
Formal proof that the protocols satisfy the service requirements