@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)",
}