http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
- 中文 을 입력하시려면 zhongwen을 입력하시고 space를누르시면됩니다.
- 北京 을 입력하시려면 beijing을 입력하시고 space를 누르시면 됩니다.
RISS 인기검색어
- 검색키워드
- 저자 : 지은경(Eun-Kyoung Jee) (검색결과 3 건)
- 무료
- 기관 내 무료
- 유료
-
실시간 모델 체커를 이용한 월성 SDS2의 명세 및 검증
지은경(Jee Eun-Kyoung),홍형석(Hong Hyoung-Seok),차성덕(Cha Sung-Deok) 한국정보과학회 2000 한국정보과학회 학술발표논문집 Vol.27 No.2Ⅰ
실시간 시스템은 그 특성상 시스템 내에서의 오류가 매우 위험하고 때론 치명적일 수 있다. 따라서, 시스템의 정확성과 안정성을 보장하는 것은 매우 중요한 문제가 된다. 이러한 문제를 해결하기 위해 정형기법을 사용한 명세와 검증을 통해 실시간 시스템의 안정성을 보장하려는 시도들이 많이 이루어져 왔다. 이 논문에서는 월성 원자로 운전 중지 시스템의 기존 명세의 문제점을 보완하여, 실시간 요구사항들을 타임드 오토마타(timed automata)로 기술할 것을 제안한다. 또한 명세를 실시간 모델 체커 UPPAAL의 입력으로 넣어서, 모델 체킹 기법을 이용해 자동적으로 시간 제약 속성을 검증한다.
-
지은경(Eun-Kyoung Jee),차성덕(Sung Deok Cha),손한성(Han Seong Son),유준범(Junbeom Yoo),구서룡(Seo-Ryong Koo),성풍현(Poong Hyun Seong) 한국정보과학회 2002 정보과학회논문지 : 소프트웨어 및 응용 Vol.29 No.11·12
폴트 트리 분석(Fault Tree Analysis)은 산업계에서 가장 널리 사용되는 안전성 분석 기법 중의 하나이다. 하지만, 이 기법은 보통 수작업으로 이루어지며, 분석 결과를 체계적이고 자동적으로 검증할 수 있는 방법이 없다는 약점을 지닌다. 본 논문에서는 실시간 모델 체커인 UPPAAL을 이용하여 안전성이 중요한 소프트웨어의 요구 사항들을 정형 명세하고, 수작업으로 완성된 폴트 트리의 정확성을 검증하는 방법을 제안하고 있다. 제안된 방법을 유용성을 확인하기 위해서 월성 원자력 발전소의 비상 정지 소프트웨어(Wolsung SDS2)에서 사용된 기능 요구 사항들을 예제로서 사용하였다. 폴트 트리는 월성 SDS2에 대한 전문적인 지식을 지니고 폴트 트리를 이용한 안전성 분석을 여러 번 수행해 본 경험이 있는 대학원생들에 의해 작성되었다. 기능 요구 사항들은 UPPAAL의 입력으로서 사용되기 위해서 시제 오토마타의 형태로 수작업으로 변환되었으며, 이 폴트 트리의 정확성을 검증하기 위해서 모델 체킹을 사용하였다. 본 논문에서 제안된 방법을 월성 SDS2 예제에 적용해 본 결과, 수작업으로 작성된 폴트 트리에 존재하는 오류를 찾을 수 있었으며, 이러한 작업을 통하여 제안된 방법이 폴트 트리 분석에 대한 신뢰도를 높이는데 유용함을 발견하였다. Fault tree analysis is the most widely used safety analysis technique in industry. However, the analysis is often applied manually, and there is no systematic and automated approach available to validate the analysis result. In this paper, we demonstrate that a real-time model checker UPPAAL is useful in formally specifying the required behavior of safety-critical software and to validate the accuracy of manually constructed fault trees. Functional requirements for emergency shutdown software for a nuclear power plant, named Wolsung SDS2, are used as an example. Fault trees were initially developed by a group of graduate students who possess detailed knowledge of Wolsung SDS2 and are familiar with safety analysis techniques including fault tree analysis. Functional requirements were manually translated in timed automata format accepted by UPPAAL, and the model checking was applied using property specifications to evaluate the correctness of the fault trees. Our application demonstrated that UPPAAL was able to detect subtle flaws or ambiguities present in fault trees. Therefore, we conclude that the proposed approach is useful in augmenting fault tree analysis.
-
연관 검색어 추천
이 검색어로 많이 본 자료
활용도 높은 자료
