Home > Research > Publications & Outputs > Sustaining property verification of synchronous...

Links

Text available via DOI:

View graph of relations

Sustaining property verification of synchronous dependable protocols over implementation

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
NullPointerException

Abstract

It is often considered that a protocol that has been verified for its dependability properties at the protocol level maintains these proven properties over its implementation. Focusing on synchronous protocols, we demonstrate that this assumption can easily be fallacious. We utilize the exumple of an existing formally verified diagnostic protocol as implemented onto the targeted time-triggered architecture (TTA). The cause is identified as the overlap mismatch across the computation and communication phases in TTA, which does not match the system assumptions of the protocol. To address this mismatch problem, we develop the concept of a generic alignment (co-ordination) layer to implement the desired communication assumptions. The verification of this layer ensures that the formally proved properties of u protocol also hold over their varied implementation. © 2007 IEEE.