Synthesis of FBD-based PLC design from NuSCR formal specification

Junbeom Yoo, Sungdeok Cha, Chang Hwoi Kim, Duck Yong Song

Research output: Contribution to journalArticle

14 Citations (Scopus)

Abstract

NuSCR is a formal specification language to document requirements for real-time embedded software with nuclear engineering applications in mind. Domain experts actively participated in selecting how to best represent various aspects. It uses tabular notations to specify required computations and automata to document state- or time-dependent behavior. As programmable logic controllers (PLCs) are widely used to implement real-time embedded software, synthesis of PLC code from a formal specification is desirable if transformation rules can be rigorously defined. In addition to improved productivity, results of safety analysis performed on requirements remain valid. In this paper, we demonstrate how NuSCR specification can be translated into semantically equivalent function block diagram (FBD) code. The process, except the initial phase where user provides information on missing or implicit details, is automated. Since executable code can be automatically generated using CASE tools from FBD, much of software development is automated. Proposed technique is currently being used in developing reactor protection system (RPS) for nuclear power plants in Korea, and experience to date has been positive. We demonstrate the proposed approach using the fixed set-point rising trip which is one of the most complex trip logics included in the RPS.

Original languageEnglish
Pages (from-to)287-294
Number of pages8
JournalReliability Engineering and System Safety
Volume87
Issue number2
DOIs
Publication statusPublished - 2005 Feb 1
Externally publishedYes

Fingerprint

Programmable Logic Controller
Logic Design
Embedded software
Formal Specification
Programmable logic controllers
Controller Design
Embedded Software
Diagram
Synthesis
Nuclear engineering
Reactor
Specification languages
Nuclear power plants
Real-time
Safety Analysis
Software engineering
Nuclear Power Plant
Fixed Point Set
Formal Languages
Productivity

Keywords

  • Design specification
  • FBD
  • Formal requirements specification
  • Nuclear power plant controller
  • PLC

ASJC Scopus subject areas

  • Mechanical Engineering
  • Safety, Risk, Reliability and Quality

Cite this

Synthesis of FBD-based PLC design from NuSCR formal specification. / Yoo, Junbeom; Cha, Sungdeok; Kim, Chang Hwoi; Song, Duck Yong.

In: Reliability Engineering and System Safety, Vol. 87, No. 2, 01.02.2005, p. 287-294.

Research output: Contribution to journalArticle

Yoo, Junbeom ; Cha, Sungdeok ; Kim, Chang Hwoi ; Song, Duck Yong. / Synthesis of FBD-based PLC design from NuSCR formal specification. In: Reliability Engineering and System Safety. 2005 ; Vol. 87, No. 2. pp. 287-294.
@article{a64a402cd10f48a69e52030f482918ec,
title = "Synthesis of FBD-based PLC design from NuSCR formal specification",
abstract = "NuSCR is a formal specification language to document requirements for real-time embedded software with nuclear engineering applications in mind. Domain experts actively participated in selecting how to best represent various aspects. It uses tabular notations to specify required computations and automata to document state- or time-dependent behavior. As programmable logic controllers (PLCs) are widely used to implement real-time embedded software, synthesis of PLC code from a formal specification is desirable if transformation rules can be rigorously defined. In addition to improved productivity, results of safety analysis performed on requirements remain valid. In this paper, we demonstrate how NuSCR specification can be translated into semantically equivalent function block diagram (FBD) code. The process, except the initial phase where user provides information on missing or implicit details, is automated. Since executable code can be automatically generated using CASE tools from FBD, much of software development is automated. Proposed technique is currently being used in developing reactor protection system (RPS) for nuclear power plants in Korea, and experience to date has been positive. We demonstrate the proposed approach using the fixed set-point rising trip which is one of the most complex trip logics included in the RPS.",
keywords = "Design specification, FBD, Formal requirements specification, Nuclear power plant controller, PLC",
author = "Junbeom Yoo and Sungdeok Cha and Kim, {Chang Hwoi} and Song, {Duck Yong}",
year = "2005",
month = "2",
day = "1",
doi = "10.1016/j.ress.2004.05.005",
language = "English",
volume = "87",
pages = "287--294",
journal = "Reliability Engineering and System Safety",
issn = "0951-8320",
publisher = "Elsevier Limited",
number = "2",

}

TY - JOUR

T1 - Synthesis of FBD-based PLC design from NuSCR formal specification

AU - Yoo, Junbeom

AU - Cha, Sungdeok

AU - Kim, Chang Hwoi

AU - Song, Duck Yong

PY - 2005/2/1

Y1 - 2005/2/1

N2 - NuSCR is a formal specification language to document requirements for real-time embedded software with nuclear engineering applications in mind. Domain experts actively participated in selecting how to best represent various aspects. It uses tabular notations to specify required computations and automata to document state- or time-dependent behavior. As programmable logic controllers (PLCs) are widely used to implement real-time embedded software, synthesis of PLC code from a formal specification is desirable if transformation rules can be rigorously defined. In addition to improved productivity, results of safety analysis performed on requirements remain valid. In this paper, we demonstrate how NuSCR specification can be translated into semantically equivalent function block diagram (FBD) code. The process, except the initial phase where user provides information on missing or implicit details, is automated. Since executable code can be automatically generated using CASE tools from FBD, much of software development is automated. Proposed technique is currently being used in developing reactor protection system (RPS) for nuclear power plants in Korea, and experience to date has been positive. We demonstrate the proposed approach using the fixed set-point rising trip which is one of the most complex trip logics included in the RPS.

AB - NuSCR is a formal specification language to document requirements for real-time embedded software with nuclear engineering applications in mind. Domain experts actively participated in selecting how to best represent various aspects. It uses tabular notations to specify required computations and automata to document state- or time-dependent behavior. As programmable logic controllers (PLCs) are widely used to implement real-time embedded software, synthesis of PLC code from a formal specification is desirable if transformation rules can be rigorously defined. In addition to improved productivity, results of safety analysis performed on requirements remain valid. In this paper, we demonstrate how NuSCR specification can be translated into semantically equivalent function block diagram (FBD) code. The process, except the initial phase where user provides information on missing or implicit details, is automated. Since executable code can be automatically generated using CASE tools from FBD, much of software development is automated. Proposed technique is currently being used in developing reactor protection system (RPS) for nuclear power plants in Korea, and experience to date has been positive. We demonstrate the proposed approach using the fixed set-point rising trip which is one of the most complex trip logics included in the RPS.

KW - Design specification

KW - FBD

KW - Formal requirements specification

KW - Nuclear power plant controller

KW - PLC

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

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

U2 - 10.1016/j.ress.2004.05.005

DO - 10.1016/j.ress.2004.05.005

M3 - Article

VL - 87

SP - 287

EP - 294

JO - Reliability Engineering and System Safety

JF - Reliability Engineering and System Safety

SN - 0951-8320

IS - 2

ER -