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
Publication date14/11/2007
Host publication10th IEEE High Assurance Systems Engineering Symposium (HASE'07)
PublisherIEEE
Pages169-178
Number of pages10
ISBN (print)0769530435, 9780769530437
<mark>Original language</mark>English

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.