Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service

Akihiro Hata, Keijiro Araki, Shigeru Kusakabe, Yoichi Omori, Hsin Hung Lin

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

Abstract

Formal methods have been used in the development of the reliable software system. However, one of the issues in using formal methods is how to model the system by considering what kind of system requirements and restrictions we should describe. In order to address this issue, we use a hazard model STAMP and an analytical method STPA based on STAMP. STAMP/STPA is proposed to overcome difficulties in approving conventional hazard analysis techniques for software-centric systems. In this report, we explain our approach and discuss our case study to develop implicit specifications for the cloud service in a model-oriented formal specification language, VDM++.

Original languageEnglish
Title of host publicationProceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages23-24
Number of pages2
ISBN (Electronic)9781479918881
DOIs
Publication statusPublished - Apr 3 2015
Event2015 2nd International Conference on Platform Technology and Service, PlatCon 2015 - Jeju, Korea, Republic of
Duration: Jan 26 2015Jan 28 2015

Publication series

NameProceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015

Other

Other2015 2nd International Conference on Platform Technology and Service, PlatCon 2015
CountryKorea, Republic of
CityJeju
Period1/26/151/28/15

Fingerprint

Hazards
Specification languages
Formal methods
Specifications
Formal specification

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Human-Computer Interaction
  • Information Systems
  • Software

Cite this

Hata, A., Araki, K., Kusakabe, S., Omori, Y., & Lin, H. H. (2015). Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service. In Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015 (pp. 23-24). [7079623] (Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/PlatCon.2015.14

Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service. / Hata, Akihiro; Araki, Keijiro; Kusakabe, Shigeru; Omori, Yoichi; Lin, Hsin Hung.

Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015. Institute of Electrical and Electronics Engineers Inc., 2015. p. 23-24 7079623 (Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015).

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

Hata, A, Araki, K, Kusakabe, S, Omori, Y & Lin, HH 2015, Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service. in Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015., 7079623, Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015, Institute of Electrical and Electronics Engineers Inc., pp. 23-24, 2015 2nd International Conference on Platform Technology and Service, PlatCon 2015, Jeju, Korea, Republic of, 1/26/15. https://doi.org/10.1109/PlatCon.2015.14
Hata A, Araki K, Kusakabe S, Omori Y, Lin HH. Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service. In Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015. Institute of Electrical and Electronics Engineers Inc. 2015. p. 23-24. 7079623. (Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015). https://doi.org/10.1109/PlatCon.2015.14
Hata, Akihiro ; Araki, Keijiro ; Kusakabe, Shigeru ; Omori, Yoichi ; Lin, Hsin Hung. / Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service. Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015. Institute of Electrical and Electronics Engineers Inc., 2015. pp. 23-24 (Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015).
@inproceedings{288285a4adf3495c9d7c42de67e68211,
title = "Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service",
abstract = "Formal methods have been used in the development of the reliable software system. However, one of the issues in using formal methods is how to model the system by considering what kind of system requirements and restrictions we should describe. In order to address this issue, we use a hazard model STAMP and an analytical method STPA based on STAMP. STAMP/STPA is proposed to overcome difficulties in approving conventional hazard analysis techniques for software-centric systems. In this report, we explain our approach and discuss our case study to develop implicit specifications for the cloud service in a model-oriented formal specification language, VDM++.",
author = "Akihiro Hata and Keijiro Araki and Shigeru Kusakabe and Yoichi Omori and Lin, {Hsin Hung}",
year = "2015",
month = "4",
day = "3",
doi = "10.1109/PlatCon.2015.14",
language = "English",
series = "Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "23--24",
booktitle = "Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015",
address = "United States",

}

TY - GEN

T1 - Using hazard analysis STAMP/STPA in developing model-oriented formal specification toward reliable cloud service

AU - Hata, Akihiro

AU - Araki, Keijiro

AU - Kusakabe, Shigeru

AU - Omori, Yoichi

AU - Lin, Hsin Hung

PY - 2015/4/3

Y1 - 2015/4/3

N2 - Formal methods have been used in the development of the reliable software system. However, one of the issues in using formal methods is how to model the system by considering what kind of system requirements and restrictions we should describe. In order to address this issue, we use a hazard model STAMP and an analytical method STPA based on STAMP. STAMP/STPA is proposed to overcome difficulties in approving conventional hazard analysis techniques for software-centric systems. In this report, we explain our approach and discuss our case study to develop implicit specifications for the cloud service in a model-oriented formal specification language, VDM++.

AB - Formal methods have been used in the development of the reliable software system. However, one of the issues in using formal methods is how to model the system by considering what kind of system requirements and restrictions we should describe. In order to address this issue, we use a hazard model STAMP and an analytical method STPA based on STAMP. STAMP/STPA is proposed to overcome difficulties in approving conventional hazard analysis techniques for software-centric systems. In this report, we explain our approach and discuss our case study to develop implicit specifications for the cloud service in a model-oriented formal specification language, VDM++.

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

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

U2 - 10.1109/PlatCon.2015.14

DO - 10.1109/PlatCon.2015.14

M3 - Conference contribution

AN - SCOPUS:84928180087

T3 - Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015

SP - 23

EP - 24

BT - Proceedings - 2015 International Conference on Platform Technology and Service, PlatCon 2015

PB - Institute of Electrical and Electronics Engineers Inc.

ER -