Zhen Zhang PhD final thesis defense



Zhen Zhang
Advisor: Chris Myers


Over the last decade, cyber-physical systems (CPSs) have seen significant applications in many safety-critical areas, such as automatic pilot avionics, autonomous automotive systems, wireless sensor networks, etc. A CPS uses networked embedded computers to monitor and control physical processes. The motivating example for this dissertation is the use of fault-tolerant routing protocol for a Network-on-Chip (NoC) architecture that connects electronic control units (ECUs) to regulate sensors and actuators in a vehicle. With a network allowing ECUs to communicate with each other, it is possible for them to share processing power to improve performance. In addition, networked ECUs enable flexible mapping to physical processes (e.g. sensors, actuators), which increases resilience to ECU failures by reassigning physical processes to spare ECUs. For the on-chip routing protocol, the ability to tolerate network faults is important for hardware reconfiguration to maintain the normal operation of a system. Adding a fault-tolerance feature in a routing protocol, however, increases its design complexity, making it prone to many functional problems. Formal verification techniques are therefore needed to verify its correctness. This dissertation proposes a link-fault tolerant, multiflit wormhole routing algorithm, and its formal modeling and verification using two different methodologies.

Improved upon the Glass and Ni’s routing algorithm that assumes node faults, this dissertation proposes a routing architecture extending that introduced by Wu et al. to a multiflit wormhole setting. It loosens Glass and Ni’s impractical assumption to achieve link-fault tolerance, covering a wider range of link fault cases that it fails to handle. Deadlock avoidance is implemented conservatively with adequate packet drops to break the cycle of dependencies. Simulation results indicate that this algorithm provides significant improvements in network reliability with minimal cost.

This link-fault routing algorithm is modeled in the process-algebraic language LNT. With the help of the CADP verification tool box, formal analysis exposes design flaws leading to false behaviors such as a packet leakage path leading to unintended packet drop and deadlock caused by removing arbiter’s buffering capacity. To combat the notorious state explosion problem, a data abstraction technique is applied to map the destination coordinates of a packet to a Boolean value representing its diversion status. Mismatch between the abstract and concrete models leads to the discovery of a potential livelock problem due to redundant packet diversions. Elimination of these diversions leads to an improved algorithm that simplifies the routing architecture, enabling successful compositional verification. The routing algorithm is proven to have several desirable properties including deadlock and livelock freedom, and tolerance to a single-link-fault.

As a comparison, the derived livelock-free routing protocol is modeled using the channel- level VHDL that is automatically compiled to labeled Petri-nets (LPNs) for verification using the LEMA tool.
Algorithms are described for an ample set based partial order reduction (POR) technique, which analyzes transition dependencies through a recursive trace-back search on LPNs. A set with the least number of enabled transitions that need interleaving is selected at each state. Cost and benefit of using trace-back are evaluated on several non-trivial asynchronous circuit models, and are compared to LNT models on a series of buffers that uses asynchronous communication. Finally, verification results are reported on using POR with trace-back on the livelock-free two-by-two NoC model.

Monday October 26, 2015
9:00 AM
ECE conference room, Merrill Engineering Building (MEB) Room 3235
The public is invited