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

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Sustaining property verification of synchronous dependable protocols over implementation

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Sustaining property verification of synchronous dependable protocols over implementation. / Bokor, P.; Serafini, M.; Sisak, Á. et al.
10th IEEE High Assurance Systems Engineering Symposium (HASE'07). IEEE, 2007. p. 169-178.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Bokor, P, Serafini, M, Sisak, Á, Pataricza, A & Suri, N 2007, Sustaining property verification of synchronous dependable protocols over implementation. in 10th IEEE High Assurance Systems Engineering Symposium (HASE'07). IEEE, pp. 169-178. https://doi.org/10.1109/HASE.2007.68

APA

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

Vancouver

Bokor P, Serafini M, Sisak Á, Pataricza A, Suri N. Sustaining property verification of synchronous dependable protocols over implementation. In 10th IEEE High Assurance Systems Engineering Symposium (HASE'07). IEEE. 2007. p. 169-178 doi: 10.1109/HASE.2007.68

Author

Bokor, P. ; Serafini, M. ; Sisak, Á. et al. / Sustaining property verification of synchronous dependable protocols over implementation. 10th IEEE High Assurance Systems Engineering Symposium (HASE'07). IEEE, 2007. pp. 169-178

Bibtex

@inproceedings{b59d70c1a2104813a4601b0dea607ce6,
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. {\textcopyright} 2007 IEEE.",
keywords = "Communication, Dynamic programming, Error analysis, Fault tolerant computer systems, Health, Industrial engineering, Laws and legislation, Systems engineering, Technical presentations, Technology, Communication phases, High assurance systems, International symposium, Mismatch problems, Property verification, Protocol level, Synchronous protocols, Time-triggered architecture, Network architecture",
author = "P. Bokor and M. Serafini and {\'A}. Sisak and A. Pataricza and Neeraj Suri",
year = "2007",
month = nov,
day = "14",
doi = "10.1109/HASE.2007.68",
language = "English",
isbn = "0769530435",
pages = "169--178",
booktitle = "10th IEEE High Assurance Systems Engineering Symposium (HASE'07)",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Sustaining property verification of synchronous dependable protocols over implementation

AU - Bokor, P.

AU - Serafini, M.

AU - Sisak, Á.

AU - Pataricza, A.

AU - Suri, Neeraj

PY - 2007/11/14

Y1 - 2007/11/14

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. © 2007 IEEE.

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. © 2007 IEEE.

KW - Communication

KW - Dynamic programming

KW - Error analysis

KW - Fault tolerant computer systems

KW - Health

KW - Industrial engineering

KW - Laws and legislation

KW - Systems engineering

KW - Technical presentations

KW - Technology

KW - Communication phases

KW - High assurance systems

KW - International symposium

KW - Mismatch problems

KW - Property verification

KW - Protocol level

KW - Synchronous protocols

KW - Time-triggered architecture

KW - Network architecture

U2 - 10.1109/HASE.2007.68

DO - 10.1109/HASE.2007.68

M3 - Conference contribution/Paper

SN - 0769530435

SN - 9780769530437

SP - 169

EP - 178

BT - 10th IEEE High Assurance Systems Engineering Symposium (HASE'07)

PB - IEEE

ER -