Review] Model Checking UML Activity Diagrams in FDR

[hckim]

논문 리뷰 기회가 되어 채점자의 입장에서 볼수 있는 좋은 기회가 되었습니다.
금요일에 랩미팅 참가가 불가하여 사전에 리뷰 결과를 올립니다. (자료는 파일란에 올리도록 하겠습니다)

저의 평가는 다음과 같습니다.

Importance (1-5) 3
Originality (1-5) 4
Technical quality (1-5) 4
References (1-5) 3
Readability and organization (1-5) 4
Overall recommendation Neutral
Reviewer's confidence level (1-3) 2

This paper describes a way to translate formal and model check in UML
ADs using CSP and FDR. The items such as initial nodes, fork-join
nodes, and etc are formalized well. Moreover, this paper prove his
translation using FDR. Initial approach of formalization in UML ADs
are well done, but it needs more future works because UML ADs has many
scenarios that can not easily be covered by utilizing formalization.

간략히 정리하면, UML 액티비티 다이어그램의 각 요소(초기노드, 브랜치, 결정 노드, 예외 핸들러등)에 대해서 Hoare의 논
리기술법으로 정리를 하였으며 FDR이라고 하는 Formal Model 해석 툴을 이용해 저자의 해석법에 대한 증명을 하였습니
다. 이해하기 쉽고 잘 정리가 되었다고 생각이 들었으나, 저자가 제시한 시나리오의 한계(시나리오가 간단함)으로 인해 더 연구가
필요하다는 생각이 들었습니다. 저자도 역시 이부분을 Future Work로 제시하고 있습니다.