Development of RTOS for PLC using formal methods

Jin Hyun Kim; Su Young Lee; Young Ah Ahn; Jae Hwan Sim; Jin Seok Yang; Na Young Lee; Jin Young Choi

doi:10.1007/978-3-540-30476-0_40

Development of RTOS for PLC using formal methods

Jin Hyun Kim, Su Young Lee, Young Ah Ahn, Jae Hwan Sim, Jin Seok Yang, Na Young Lee, Jin Young Choi

School of Cybersecurity

Research output: Chapter in Book/Report/Conference proceeding › Chapter

1 Citation (Scopus)

Abstract

Programmable logic controller(PLC) is a computer system for instrumentation and control (I&C) systems such as control of machinery on factory assembly lines and nuclear power plants. If PLC is used to control core reactor in nuclear power plant, it should be classified into safety-critical. PLC has various I&C logics made in software, including real-time operating system (RTOS). Hence, RTOS must be also proved completely. In this paper, we apply formal methods to a development of RTOS for PLC.which is developing in Korean national nuclear project,in safety-critical level; Statecharts for specification and model checking for verification, and we give the results of applying formal methods to RTOS.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Farn Wang
Publisher	Springer Verlag
Pages	479-482
Number of pages	4
ISBN (Print)	9783540236108
DOIs	https://doi.org/10.1007/978-3-540-30476-0_40
Publication status	Published - 2004

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3299
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-30476-0_40

Cite this

Kim, J. H., Lee, S. Y., Ahn, Y. A., Sim, J. H., Yang, J. S., Lee, N. Y., & Choi, J. Y. (2004). Development of RTOS for PLC using formal methods. In F. Wang (Ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 479-482). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3299). Springer Verlag. https://doi.org/10.1007/978-3-540-30476-0_40

Development of RTOS for PLC using formal methods. / Kim, Jin Hyun; Lee, Su Young; Ahn, Young Ah et al.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Farn Wang. Springer Verlag, 2004. p. 479-482 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3299).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Kim, JH, Lee, SY, Ahn, YA, Sim, JH, Yang, JS, Lee, NY & Choi, JY 2004, Development of RTOS for PLC using formal methods. in F Wang (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3299, Springer Verlag, pp. 479-482. https://doi.org/10.1007/978-3-540-30476-0_40

Kim JH, Lee SY, Ahn YA, Sim JH, Yang JS, Lee NY et al. Development of RTOS for PLC using formal methods. In Wang F, editor, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2004. p. 479-482. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-30476-0_40

Kim, Jin Hyun ; Lee, Su Young ; Ahn, Young Ah et al. / Development of RTOS for PLC using formal methods. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Farn Wang. Springer Verlag, 2004. pp. 479-482 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{17109b7499124c59b22c52bbbfd000f5,

title = "Development of RTOS for PLC using formal methods",

abstract = "Programmable logic controller(PLC) is a computer system for instrumentation and control (I&C) systems such as control of machinery on factory assembly lines and nuclear power plants. If PLC is used to control core reactor in nuclear power plant, it should be classified into safety-critical. PLC has various I&C logics made in software, including real-time operating system (RTOS). Hence, RTOS must be also proved completely. In this paper, we apply formal methods to a development of RTOS for PLC.which is developing in Korean national nuclear project,in safety-critical level; Statecharts for specification and model checking for verification, and we give the results of applying formal methods to RTOS.",

author = "Kim, {Jin Hyun} and Lee, {Su Young} and Ahn, {Young Ah} and Sim, {Jae Hwan} and Yang, {Jin Seok} and Lee, {Na Young} and Choi, {Jin Young}",

year = "2004",

doi = "10.1007/978-3-540-30476-0_40",

language = "English",

isbn = "9783540236108",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "479--482",

editor = "Farn Wang",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Development of RTOS for PLC using formal methods

AU - Kim, Jin Hyun

AU - Lee, Su Young

AU - Ahn, Young Ah

AU - Sim, Jae Hwan

AU - Yang, Jin Seok

AU - Lee, Na Young

AU - Choi, Jin Young

PY - 2004

Y1 - 2004

N2 - Programmable logic controller(PLC) is a computer system for instrumentation and control (I&C) systems such as control of machinery on factory assembly lines and nuclear power plants. If PLC is used to control core reactor in nuclear power plant, it should be classified into safety-critical. PLC has various I&C logics made in software, including real-time operating system (RTOS). Hence, RTOS must be also proved completely. In this paper, we apply formal methods to a development of RTOS for PLC.which is developing in Korean national nuclear project,in safety-critical level; Statecharts for specification and model checking for verification, and we give the results of applying formal methods to RTOS.

AB - Programmable logic controller(PLC) is a computer system for instrumentation and control (I&C) systems such as control of machinery on factory assembly lines and nuclear power plants. If PLC is used to control core reactor in nuclear power plant, it should be classified into safety-critical. PLC has various I&C logics made in software, including real-time operating system (RTOS). Hence, RTOS must be also proved completely. In this paper, we apply formal methods to a development of RTOS for PLC.which is developing in Korean national nuclear project,in safety-critical level; Statecharts for specification and model checking for verification, and we give the results of applying formal methods to RTOS.

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

U2 - 10.1007/978-3-540-30476-0_40

DO - 10.1007/978-3-540-30476-0_40

M3 - Chapter

AN - SCOPUS:35048893500

SN - 9783540236108

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 479

EP - 482

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Wang, Farn

PB - Springer Verlag

ER -

Development of RTOS for PLC using formal methods

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this