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 |
|---|---|
| Pages (from-to) | 479-482 |
| Number of pages | 4 |
| Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Volume | 3299 |
| Publication status | Published - 2004 Dec 1 |
Fingerprint
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 journal › Article
}
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 -