Synthesis of FBD-based PLC design from NuSCR formal specification

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

Research output: Contribution to journalArticlepeer-review

15 Citations (Scopus)


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
Issue number2
Publication statusPublished - 2005 Feb
Externally publishedYes


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

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Industrial and Manufacturing Engineering


Dive into the research topics of 'Synthesis of FBD-based PLC design from NuSCR formal specification'. Together they form a unique fingerprint.

Cite this