Home > Research > Publications & Outputs > Aiding modular design and verification of safet...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications

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

Published

Standard

Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications. / Sakurai, K.; Bokor, P.; Suri, Neeraj.
2008 11th IEEE High Assurance Systems Engineering Symposium. IEEE, 2008. p. 261-270.

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

Harvard

Sakurai, K, Bokor, P & Suri, N 2008, Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications. in 2008 11th IEEE High Assurance Systems Engineering Symposium. IEEE, pp. 261-270. https://doi.org/10.1109/HASE.2008.45

APA

Sakurai, K., Bokor, P., & Suri, N. (2008). Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications. In 2008 11th IEEE High Assurance Systems Engineering Symposium (pp. 261-270). IEEE. https://doi.org/10.1109/HASE.2008.45

Vancouver

Sakurai K, Bokor P, Suri N. Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications. In 2008 11th IEEE High Assurance Systems Engineering Symposium. IEEE. 2008. p. 261-270 doi: 10.1109/HASE.2008.45

Author

Sakurai, K. ; Bokor, P. ; Suri, Neeraj. / Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications. 2008 11th IEEE High Assurance Systems Engineering Symposium. IEEE, 2008. pp. 261-270

Bibtex

@inproceedings{dcd0bb35ca8c4dbfb3e6685f18f96078,
title = "Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications",
abstract = "Designing safety-critical systems is a complex process, and especially when the design is carried out at different levels of abstraction where the correctness of the design at one level is not automatically sustained over the next level. In this work we focus on time-triggered (TT) systems where the resources of communication and computation are shared among different applications to reduce the overall cost of the system. This entails serializing both communication and computation which does not necessarily meet the assumptions made by the application. Hence, we present the concept of executable formal specification of general TT systems to establish a faithful model of the TT characteristics. Our focus is on general applications running in a synchronous environment. The proposed model can be easily customized by the user and it is able to support simulation and verification of the system. It also aids the effective deployment of applications, and the validation of the real system with model-based test generation. Our case study shows how the general model can be implemented in the SAL language and how SAL's tool suite can be used to guide the design of general TT systems. {\textcopyright} 2008 IEEE.",
keywords = "Applications, Formal logic, Safety engineering, Specifications, Systems engineering, Case studies, Complex processing, Formal specifications, General applications, General model, Real systems, Test generations, Tool suite, Design",
author = "K. Sakurai and P. Bokor and Neeraj Suri",
year = "2008",
month = dec,
day = "3",
doi = "10.1109/HASE.2008.45",
language = "English",
isbn = "9780769534824",
pages = "261--270",
booktitle = "2008 11th IEEE High Assurance Systems Engineering Symposium",
publisher = "IEEE",

}

RIS

TY - GEN

T1 - Aiding modular design and verification of safety-critical time-triggered systems by use of executable formal specifications

AU - Sakurai, K.

AU - Bokor, P.

AU - Suri, Neeraj

PY - 2008/12/3

Y1 - 2008/12/3

N2 - Designing safety-critical systems is a complex process, and especially when the design is carried out at different levels of abstraction where the correctness of the design at one level is not automatically sustained over the next level. In this work we focus on time-triggered (TT) systems where the resources of communication and computation are shared among different applications to reduce the overall cost of the system. This entails serializing both communication and computation which does not necessarily meet the assumptions made by the application. Hence, we present the concept of executable formal specification of general TT systems to establish a faithful model of the TT characteristics. Our focus is on general applications running in a synchronous environment. The proposed model can be easily customized by the user and it is able to support simulation and verification of the system. It also aids the effective deployment of applications, and the validation of the real system with model-based test generation. Our case study shows how the general model can be implemented in the SAL language and how SAL's tool suite can be used to guide the design of general TT systems. © 2008 IEEE.

AB - Designing safety-critical systems is a complex process, and especially when the design is carried out at different levels of abstraction where the correctness of the design at one level is not automatically sustained over the next level. In this work we focus on time-triggered (TT) systems where the resources of communication and computation are shared among different applications to reduce the overall cost of the system. This entails serializing both communication and computation which does not necessarily meet the assumptions made by the application. Hence, we present the concept of executable formal specification of general TT systems to establish a faithful model of the TT characteristics. Our focus is on general applications running in a synchronous environment. The proposed model can be easily customized by the user and it is able to support simulation and verification of the system. It also aids the effective deployment of applications, and the validation of the real system with model-based test generation. Our case study shows how the general model can be implemented in the SAL language and how SAL's tool suite can be used to guide the design of general TT systems. © 2008 IEEE.

KW - Applications

KW - Formal logic

KW - Safety engineering

KW - Specifications

KW - Systems engineering

KW - Case studies

KW - Complex processing

KW - Formal specifications

KW - General applications

KW - General model

KW - Real systems

KW - Test generations

KW - Tool suite

KW - Design

U2 - 10.1109/HASE.2008.45

DO - 10.1109/HASE.2008.45

M3 - Conference contribution/Paper

SN - 9780769534824

SP - 261

EP - 270

BT - 2008 11th IEEE High Assurance Systems Engineering Symposium

PB - IEEE

ER -