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


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

Publication date14/11/2007
Host publication10th IEEE High Assurance Systems Engineering Symposium (HASE'07)
Number of pages10
ISBN (Print)0769530435, 9780769530437
<mark>Original language</mark>English


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.