Development of a verification method for the FBD-style design specification using ESDT and SMV = ESDT와 SMV를 이용한 FBD-style 설계명세서를 위한 검증 방법 개발

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 328
  • Download : 0
As PLCs are widely used in the digital I&C systems of nuclear power plants (NPPs), the safety of PLC software has become the most important consideration. Software safety is an important property for safety critical systems, especially those in aerospace, satellite and nuclear power plants, whose failure could result in danger to human life, property or environment. It is recently becoming more important due to the increase in the complexity and size of safety critical systems. This approach proposes a method to perform effective verification activities on the traceability analysis and software design evaluation in the software design phase. In order to perform the traceability analysis between a Software Requirements Specification (SRS) written in a natural language and a Software Design Specification (SDS) written in Function Block Diagram (FBD), this method uses extended-structured decision tables (ESDTs). ESDTs include information related to the traceability analysis from a text-based SRS and a FBD-based SDS, respectively. Through comparing with both ESDTs from a SRS and ESDTs from a SDS, the effective traceability analysis of both a text-based SRS and a FBD-based SDS can be achieved. For the software design evaluation, a model checking which is mainly used to verify PLC programs formally is used in this research. A FBD-style design specification is translated into input languages of the SMV by translation rules and then the FBD-style design specification can be formally analyzed using SMV.
Seong, Poong-Hyunresearcher성풍현researcher
한국과학기술원 : 원자력및양자공학과,
Issue Date
237980/325007  / 020023308

학위논문(석사) - 한국과학기술원 : 원자력및양자공학과, 2004.2, [ vii, 74 p. ]


Traceability Analysis; Symbolic Model Verifier; Function Block Diagram; verification; Software Design Specification; 소프트웨어 설계사양서; 추적성 분석; 모델 체킹; 기능 블럭 선도; 소프트웨어 검증

Appears in Collection
Files in This Item
There are no files associated with this item.


  • mendeley


rss_1.0 rss_2.0 atom_1.0