Home > Research > Publications & Outputs > On the use of formal techniques for analyzing d...

Research

Links

Text available via DOI:

Keywords

View graph of relations

On the use of formal techniques for analyzing dependable real-time protocols

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

Published

Standard

On the use of formal techniques for analyzing dependable real-time protocols. / Sinha, Purnendu; Suri, Neeraj.
Proceedings 20th IEEE Real-Time Systems Symposium. IEEE, 1999. p. 126-135.

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

Harvard

Sinha, P & Suri, N 1999, On the use of formal techniques for analyzing dependable real-time protocols. in Proceedings 20th IEEE Real-Time Systems Symposium. IEEE, pp. 126-135, 20th IEEE Real-Time Systems Symposium, Phoenix, Arizona, United States, 1/12/99. https://doi.org/10.1109/REAL.1999.818834

APA

Sinha, P., & Suri, N. (1999). On the use of formal techniques for analyzing dependable real-time protocols. In Proceedings 20th IEEE Real-Time Systems Symposium (pp. 126-135). IEEE. https://doi.org/10.1109/REAL.1999.818834

Vancouver

Sinha P, Suri N. On the use of formal techniques for analyzing dependable real-time protocols. In Proceedings 20th IEEE Real-Time Systems Symposium. IEEE. 1999. p. 126-135 doi: 10.1109/REAL.1999.818834

Author

Sinha, Purnendu ; Suri, Neeraj. / On the use of formal techniques for analyzing dependable real-time protocols. Proceedings 20th IEEE Real-Time Systems Symposium. IEEE, 1999. pp. 126-135

Bibtex

@inproceedings{7c9c6bc195044bb2aa0155d4345f6aab,
title = "On the use of formal techniques for analyzing dependable real-time protocols",
abstract = "The effective design of composite dependable and real-time protocols entails demonstrating their proof of correctness and, in practice, the efficient delivery of services. We focus on these aspects of correctness and efficiency, specifically considering the real-time aspects where the need is to ensure satisfaction of stringent timing and operational constraints. In this paper we establish the use of mathematically rigorous techniques such as formal methods (FM's) in not only providing for their traditional usage in establishing correctness checks, but also for their capability of assessing and analyzing timing requirements in dependable real-time protocols. We present our perspectives in utilizing FM's in developing exact case analyses of fault-tolerant and real-time protocols. We discuss the insights obtained and flaws identified in the hand analysis over the process of formally analyzing and verifying the correctness of an existing fault-tolerant real-time scheduling protocol.",
keywords = "Algorithms, Fault tolerant computer systems, Formal logic, Mathematical models, Network protocols, Numerical analysis, Scheduling, Formal methods, Rate monotonic algorithm, Real time systems",
author = "Purnendu Sinha and Neeraj Suri",
year = "1999",
month = dec,
day = "1",
doi = "10.1109/REAL.1999.818834",
language = "English",
isbn = "0769504752",
pages = "126--135",
booktitle = "Proceedings 20th IEEE Real-Time Systems Symposium",
publisher = "IEEE",
note = "20th IEEE Real-Time Systems Symposium ; Conference date: 01-12-1999 Through 03-12-1999",

}

RIS

TY - GEN

T1 - On the use of formal techniques for analyzing dependable real-time protocols

AU - Sinha, Purnendu

AU - Suri, Neeraj

PY - 1999/12/1

Y1 - 1999/12/1

N2 - The effective design of composite dependable and real-time protocols entails demonstrating their proof of correctness and, in practice, the efficient delivery of services. We focus on these aspects of correctness and efficiency, specifically considering the real-time aspects where the need is to ensure satisfaction of stringent timing and operational constraints. In this paper we establish the use of mathematically rigorous techniques such as formal methods (FM's) in not only providing for their traditional usage in establishing correctness checks, but also for their capability of assessing and analyzing timing requirements in dependable real-time protocols. We present our perspectives in utilizing FM's in developing exact case analyses of fault-tolerant and real-time protocols. We discuss the insights obtained and flaws identified in the hand analysis over the process of formally analyzing and verifying the correctness of an existing fault-tolerant real-time scheduling protocol.

AB - The effective design of composite dependable and real-time protocols entails demonstrating their proof of correctness and, in practice, the efficient delivery of services. We focus on these aspects of correctness and efficiency, specifically considering the real-time aspects where the need is to ensure satisfaction of stringent timing and operational constraints. In this paper we establish the use of mathematically rigorous techniques such as formal methods (FM's) in not only providing for their traditional usage in establishing correctness checks, but also for their capability of assessing and analyzing timing requirements in dependable real-time protocols. We present our perspectives in utilizing FM's in developing exact case analyses of fault-tolerant and real-time protocols. We discuss the insights obtained and flaws identified in the hand analysis over the process of formally analyzing and verifying the correctness of an existing fault-tolerant real-time scheduling protocol.

KW - Algorithms

KW - Fault tolerant computer systems

KW - Formal logic

KW - Mathematical models

KW - Network protocols

KW - Numerical analysis

KW - Scheduling

KW - Formal methods

KW - Rate monotonic algorithm

KW - Real time systems

U2 - 10.1109/REAL.1999.818834

DO - 10.1109/REAL.1999.818834

M3 - Conference contribution/Paper

SN - 0769504752

SP - 126

EP - 135

BT - Proceedings 20th IEEE Real-Time Systems Symposium

PB - IEEE

T2 - 20th IEEE Real-Time Systems Symposium

Y2 - 1 December 1999 through 3 December 1999

ER -