Sustaining property verification of synchronous dependable protocols over implementation

Péter Bokor, Marco Serafini, Áron Sisak, András Pataricza, Neeraj Suri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings of IEEE International Symposium on High Assurance Systems Engineering
Pages169-178
Number of pages10
DOIs
Publication statusPublished - 1 Dec 2007
Externally publishedYes
Event10th IEEE International Symposium on High Assurance Systems Engineering, HASE 2007 - Dallas, TX, United States
Duration: 14 Nov 200716 Nov 2007

Other

Other10th IEEE International Symposium on High Assurance Systems Engineering, HASE 2007
CountryUnited States
CityDallas, TX
Period14/11/0716/11/07

Fingerprint

Network protocols
Communication

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Bokor, P., Serafini, M., Sisak, Á., Pataricza, A., & Suri, N. (2007). Sustaining property verification of synchronous dependable protocols over implementation. In Proceedings of IEEE International Symposium on High Assurance Systems Engineering (pp. 169-178). [4404739] https://doi.org/10.1109/HASE.2007.68

Sustaining property verification of synchronous dependable protocols over implementation. / Bokor, Péter; Serafini, Marco; Sisak, Áron; Pataricza, András; Suri, Neeraj.

Proceedings of IEEE International Symposium on High Assurance Systems Engineering. 2007. p. 169-178 4404739.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bokor, P, Serafini, M, Sisak, Á, Pataricza, A & Suri, N 2007, Sustaining property verification of synchronous dependable protocols over implementation. in Proceedings of IEEE International Symposium on High Assurance Systems Engineering., 4404739, pp. 169-178, 10th IEEE International Symposium on High Assurance Systems Engineering, HASE 2007, Dallas, TX, United States, 14/11/07. https://doi.org/10.1109/HASE.2007.68
Bokor P, Serafini M, Sisak Á, Pataricza A, Suri N. Sustaining property verification of synchronous dependable protocols over implementation. In Proceedings of IEEE International Symposium on High Assurance Systems Engineering. 2007. p. 169-178. 4404739 https://doi.org/10.1109/HASE.2007.68
Bokor, Péter ; Serafini, Marco ; Sisak, Áron ; Pataricza, András ; Suri, Neeraj. / Sustaining property verification of synchronous dependable protocols over implementation. Proceedings of IEEE International Symposium on High Assurance Systems Engineering. 2007. pp. 169-178
@inproceedings{fda67bace5df4caeb4ae17549bb14788,
title = "Sustaining property verification of synchronous dependable protocols over implementation",
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.",
author = "P{\'e}ter Bokor and Marco Serafini and {\'A}ron Sisak and Andr{\'a}s Pataricza and Neeraj Suri",
year = "2007",
month = "12",
day = "1",
doi = "10.1109/HASE.2007.68",
language = "English",
isbn = "0769530435",
pages = "169--178",
booktitle = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",

}

TY - GEN

T1 - Sustaining property verification of synchronous dependable protocols over implementation

AU - Bokor, Péter

AU - Serafini, Marco

AU - Sisak, Áron

AU - Pataricza, András

AU - Suri, Neeraj

PY - 2007/12/1

Y1 - 2007/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=48349146090&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=48349146090&partnerID=8YFLogxK

U2 - 10.1109/HASE.2007.68

DO - 10.1109/HASE.2007.68

M3 - Conference contribution

SN - 0769530435

SN - 9780769530437

SP - 169

EP - 178

BT - Proceedings of IEEE International Symposium on High Assurance Systems Engineering

ER -