Application of statecharts and table methods to formal specification of the NPP trip function requirements = 원자력발전소 트립기능 요건의 정형적 명세를 위한 Statecharts와 테이블 방법 응용에 관한 연구

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 279
  • Download : 0
This paper presents the results of study which develops the formal specification of the trip function requirements of SDS2 that is a safety critical system using an integrated formal approach that combines the statecharts and the table notation methods. A visual formal notation, statecharts, is used to specify the requirements of the simplified SDS2. As background, the statechart approach to specifying requirements is reviewed. A table notation method is used to cope with the limitation of the statecharts. A table notation editor is designed to provide the automatic checking of the correct usage of the variables and to verify the correctness of the computational parts of the requirements. The developed specification is executed graphically using a simulator to ensure that it captures the intended behaviors of the system. The formal specification is analyzed statically for syntactic correctness and dynamically for potential errors. It is found that the formal specification makes it easier to detect incomplete specifications, specification errors or inconsistencies at an early stage. In conclusion, it is believed that a great increase in confidence in the system can be obtained by the use of formal specifications at early requirements stage of the software life cycles.
Advisors
Seong, Poong-Hyunresearcher성풍현researcher
Description
한국과학기술원 : 원자력공학과,
Publisher
한국과학기술원
Issue Date
1999
Identifier
150470/325007 / 000943269
Language
eng
Description

학위논문(석사) - 한국과학기술원 : 원자력공학과, 1999, [ iv, 73 p. ]

Keywords

Statecharts; Formal specification; Formal methods; Table notation; 테이블방법; 스테이트차트; 정형적 명세; 정형적 방법론

URI
http://hdl.handle.net/10203/49390
Link
http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=150470&flag=dissertation
Appears in Collection
NE-Theses_Master(석사논문)
Files in This Item
There are no files associated with this item.

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0