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

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)479-482
Number of pages4
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3299
Publication statusPublished - 2004 Dec 1

Fingerprint

Programmable Logic Controller
Formal methods
Computer Systems
Formal Methods
Programmable logic controllers
Operating Systems
Real-time
Nuclear Power Plant
Nuclear Power Plants
Nuclear power plants
Safety
Statecharts
Assembly Line
Reactor cores
Model checking
Instrumentation
Reactor
Model Checking
Machinery
Industrial plants

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Development of RTOS for PLC using formal methods. / Kim, Jin Hyun; Lee, Su Young; Ahn, Young Ah; Sim, Jae Hwan; Yang, Jin Seok; Lee, Na Young; Choi, Jin Young.

In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 3299, 01.12.2004, p. 479-482.

Research output: Contribution to journalArticle

Kim, Jin Hyun ; Lee, Su Young ; Ahn, Young Ah ; Sim, Jae Hwan ; Yang, Jin Seok ; Lee, Na Young ; Choi, Jin Young. / Development of RTOS for PLC using formal methods. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2004 ; Vol. 3299. pp. 479-482.
@article{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",
month = "12",
day = "1",
language = "English",
volume = "3299",
pages = "479--482",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

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/12/1

Y1 - 2004/12/1

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

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

M3 - Article

AN - SCOPUS:35048893500

VL - 3299

SP - 479

EP - 482

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

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

SN - 0302-9743

ER -