DONG-AH LEE Researcher / Ph.D

Dependable Software Laboratory [link]
Department of Computer Science and Engineering [link]
Konkuk University [link]
Republic of Korea

E-Mail: ldalove@konkuk.ac.kr

Research Interests

• Formal verification
• Safety/hazard analysis
• Dependable systems

Education

• Aug 2019 Ph.D. in Computer and Information Communication Engineering
  • Dependable Software Laboratory
  • KONKUK University
  • Dissertation title: A formal verification framework using Traceability-based Selective Model Projection for Large-scale Software
    • Advisor: Junbeom Yoo
• Feb 2012 M.S. in Computer and Information Communication Engineering
  • Dependable Software Laboratory
  • KONKUK University
  • Thesis title: Verification of Behavioral Consistency between FBD and C programs using HW-CBMC [link]
    • Advisor: Junbeom Yoo
• Feb 2010 B.S. in Computer Science and Engineering
  • KONKUK University

Publications

International Journal

• Dong-Ah Lee, Sangkyung Sung, Junbeom Yoo and Doo-Hyun Kim, "Formal Modeling and Verification of Operational Flight Program in a Small-Scale Unmanned Helicopter," Journal of Aerospace Engineering, Vol.25, No.4, pp.530–540, 2012. [Paper]
• Dong-Ah Lee, Junbeom Yoo and Jang-Soo Lee, "A Systematic Verification of Behavioral Consistency between FBD Design and ANSI-C Implementation Using HW-CBMC," Reliability Engineering and System Safety, Available online, 2 July 2013. [Paper]
• Eui-Sub Kim, Dong-Ah Lee, Sejin Jung, Junbeom Yoo, Jong-Gyun Choi, Jang-Soo Lee "NuDE 2.0: A Formal Method-based Software Development, Verification and Safety Analysis Environment for Digital I&Cs in NPPs," Journal of Computing Science and Engineering, Vol.11, No.1, pp.9-23, 2017. [paper]
• Sanghyun Yoon, Dong-Ah Lee, Eunji Pak, Taeho Kim and Junbeom Yoo, "Timed Model-based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 compliance RTOS," IEICE Transactions on Information and Systems, Vol.E100-D, No.10, pp.2644-2647, 2017. [paper]
• Dong-Ah Lee, Eui-Sub Kim, and Junbeom Yoo, "Quantitative Measures of the Thoroughness of FBD Simulations for PLC-based Digital I&C System," Nuclear Engineering and Technology, 2020. [paper]
• Dong-Ah Lee, Eui-Sub Kim, and Junbeom Yoo, "An Empirical Evaluation of Coverage Criteria for FBD Simulation using Mutation Analysis," IEICE Transactions on Information and Systems, Vol.E104-D, No.01, pp.-, Jan. 2021. [paper]

International Conference

• Dong-Ah Lee, Junbeom Yoo, and Doohyun Kim, "Formal Verification of Process Communications in Operational Flight Program for a Small-Scale Unmanned Helicopter," The 6th International Conference on Intelligent Unmanned Systems (ICIUS 2010), pp.91–96, Nov. 3–5, Bali, Indonesia, 2010. [Paper, Presentation]
• Dong-Ah Lee, Junbeom Yoo, and Jang-Soo Lee, "Equivalence Checking between Function Block Diagrams and C Programs using HW-CBMC," The 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011), LNCS 6894, pp.397–408, Sept. 19–21, Naples, Italy, 2011. [Paper, Presentation]
• Dong-Ah Lee, Jong-Hoon Lee, Junbeom Yoo, and Doo-Hyun Kim, "Systematic Verification of Operational Flight Program through Reverse Engineering," In Proceeding of Software Engineering, Business Continuity, ad Education (CCIS 257), The 3rd International Mega-Conference on Future Generation Information Technology (FGIT 2011); International Conference on Advanced Software Engineering and its Application 2011 (ASEA 2011), pp.285–291, Dec. 08–10, Jeju, Korea, 2011. [Paper, Presentation]
• Eui-Sub Kim, Dong-Ah Lee, and Junbeom Yoo, "RT-Selection : A Regression Test Selection Technique Using Textual Differencing and Change Impact Analysis," 2013 International Workshop on ICT, pp.1–4, Dec. 12–14, Beppu, Japan, 2013. [paper, Presentation]
• Dong-Ah Lee, Eui-sub Kim, Junbeom Yoo, Jang-Soo Lee, and Jong Gyun Choi, "FBDtoVerilog 2.0: An automatic translation of FBD into Verilog to develop FPGA," International Conference on Information Science & Applications 2014 (ICISA2014), pp. 447–450, May 6th–9th, Seoul, Republic of Korea, 2014 [Paper, Presentation]
• Junbeom Yoo, Eui-Sub Kim, Dong-Ah Lee, and Jong-Gyun Choi, "An Integrated Software Development Framework for PLC & FPGA based Digital I&Cs," International Symposium on Future I&C for Nuclear Power Plants (ISOFIC/ISSNP 2014), Aug. 25-28, Jeju, Republic of Korea, 2014. [Paper, Presentation]
• Dong-Ah Lee, Junbeom Yoo and Jang-Soo Lee, "Guidelines for the Use of the Function Block Diagram in Reactor Protection Systems," The 21st Asia-Pacific Software Engineering Conference (APSEC 2014), pp.141–149 Dec. 1–4, Jeju, Republic of Korea, 2014. [Paper, Presentation]
• Junbeom Yoo, Eui-Sub Kim, Dong-Ah Lee, Jong-Gyun Choi, Young Jun Lee and Jang-Soo Lee, "NuDE 2.0: A Model-based Software Development Environment for the PLC & FPGA based Digital Systems in Nuclear Power Plants," International Symposium on Integrated Circuit (ISIC 2014), pp.00–00, Dec. 10–12, Singapore, 2014. [Paper, Presentation]

Domestic Journal & Magazine

• 이동아, 김의섭, 유준범, "원자력 발전소 I&C 시스템의 안전성 분석을 위한 신기술 적용 사례", 정보과학회지, 제31권, 제5호, pp. 10-17, 2013. [Paper]
• 김의섭, 이동아, 유준범, "RT-Selection: 텍스트 차이점과 변경 영향 분석을 이용한 회귀 테스트 선택 기법", 정보과학회논문지 : 소프트웨어 및 응용, 제41권, 제6호, pp. 407-416, 2014. [Paper]
• 김의섭, 이동아, 유준범, "RT-Selection: 텍스트 차이점과 변경 영향 분석을 이용한 회귀 테스트 선택 기법", 소프트웨어공학센터 웹진 108호, 2014. [Paper]
• 이동아, 유준범, 최종균, "원자력 발전소의 FPGA 기반 계측제어 시스템을 위한 통합 소프트웨어 개발 환경", 정보과학회지 제32권 제12호 통권 제307호, pp. 36-43, 2014. [Paper]
• 이장수, 이동아, "소프트웨어 기반의 안전 필수 시스템을 위한 안전성 분석 기법", 정보과학회지, 제 33권, 제 7호, pp. 41-46, 2015. [Paper]
• 정세진, 이동아, 김의섭, 장천현, 유준범, "OOPT: 소프트웨어공학 교육을 위한 객체지향 소프트웨어 개발 방법론", 정보과학회논문지, 제 44권, 제 5호, pp. 510-521, 2017. [paper]
• 이동아, 유준범, "FMProjector: 표준 인터페이스를 준수하는 운영체제를 위한 정형 검증 프레임워크", 한국정보과학회논문지, 제 46권, 제 8호, pp. 814-822, 2019.08. [paper]

Domestic Conference

• 김영호, 이동아, 윤상현, 박윤정, 민덕기, "아이팟 모바일 캘린더 및 주소록 프로그램을 이용한 상용 엡서버 동기화 시스템", 제 32회 한국정보처리학회 추계학술발표대회, 16권, 2호, p123-124, 건국대학교 서울캠퍼스, 2009.11.01 [Paper]
• Sanghyun Yun, Dong-Ah Lee, and Junbeom Yoo, "NuFTA: A CASE Tool for Automatic Software Fault Tree Analysis," Transactions of the Korean Nuclear Society Spring Meeting 2010, pp.855–856, May 27–28, Pyeongchang, Korea, 2010. [Paper, Poster]
• 이동아, 윤상현, 이무열, 진현욱, 유준범, "SPIN을 이용한 차량용 MOST Network Service 프로토콜 스택 정형검증", 한국정보과학회 2010 한국컴퓨터종합학술대회, Vol. 37, No.1(A), p60~61, 제주대, 2010.06.30~07.02 [Paper, Presentation]
• 이종훈, 이동아, 유준범, "HELISCOPE Project 의 비행 운용 프로그램을 위한 검증 절차," 2011 한국소프트웨어공학학술대회 (KCSE 2011), pp.303~311, 강원도 보광 휘닉스파크, 2011. [Paper, Presentation]
• Dong-Ah Lee, Jong-Hoon Lee, and Junbeom Yoo, "Verification Process of Behavioral Consistency between Design and Implementation programs of pSET using HW-CBMC," Transactions of the Korean Nuclear Society Spring Meeting 2011, pp.933–934, May 26–27, Taebaek, Korea, 2011.[Paper, Presentation]
• 이동아, 유준범, "pSET 저장형식의 표준화를 위한 변환도구 개발: pSET2TC6", 한국정보과학회 제38회 추계학술발표회 (KIISE 2011), 서울 서울대학교, Vol. 38, No.2(B), pp.105~107, 2011.11.25~26 [Paper, Poster]
• 이종훈, 이동아, 유준범, 송승화, 김두현, "소프트웨어 역공학을 통한 HeliScope OFP의 테스트 케이스 생성", 2012 한국소프트웨어공학학술대회(KCSE 2012), 강원도 보광 휘닉스파크, 2012.2.8~10 [Paper, Presentation]
• 이동아, 김의섭, 유준범, "고장수목을 이용한 Function Block Diagram의 위험성 분석 기법 연구", 2012 한국정보과학회 학술발표논문집, 충남대학교, Vol. 39, No. 2(B), pp. 76~78, 2012. [Paper, Presentation]
• 김의섭, 이동아, 유준범, "번역기, 코드 생성기 및 컴파일러를 위한 검증기법 조사", 제 15회 한국 소프트웨어공학 학술대회(KCSE 2013), Vol. 15, No. 1, pp. 43~51, 강원도 평창 휘닉스파크, 2013.01.30~02.01 [Paper, Presentation]
• 서영주, 이동아, 유준범, "Fault Tree의 저장을 위한 범용적인 형태의 XML 스키마", 한국정보과학회 2013 한국컴퓨터종합학술대회 논문집, pp. 592~594, 전라남도 여수 디오션리조트, 2013.06.26~28 [Paper, Poster, Prize]
• 이동아, 김의섭, 서영주, 유준범, "FBDEditor: 원자력 계측제어 시스템 개발을 위한 FBD 설계 프로그램", 2014 한국소프트웨어공학학술대회 (KCSE 2014), pp.315-318, 강원도 평창 휘닉스파크, 02.12~02.14, 2014. [Paper, Presentation]
• 김의섭, 이동아, 유준범, "FBDtoVerilog 변환기의 Correctness 를 검증하기 위한 자동화된 시나리오 생성기 구현", 2014 한국정보처리학회 춘계학술발표대회 (KIPS 2014) 논문집 제21권 1호, pp.599-602, 아주대학교, 04.24~25, 2014. [Paper, Presentation]
• 서영주, 이동아, 유준범, "VerilogLinker : FPGA제어기 통합개발환경과 상용 FPGA 합성도구의 연동", 2014 한국정보처리학회 춘계학술발표대회 (KIPS 2014) 논문집 제21권 1호, pp.595-599, 아주대학교, 04.24~25, 2014. [Paper, Presentation]
• 김재엽, 이동아, 서영주, 유준범, "NuSCRtoFBD 4.0: NuSCR 정형명세언어로부터 FPGA 개발용 FBD프로그램 자동생성 도구", 2014년 한국컴퓨터종합학술대회 논문집 (KCC 2014), pp 1986-1988, 부경대학교&해운대그랜드호텔, 06.25-06.27, 2014. [Paper, Presentation]
• Sejin Jung, Dong-Ah Lee, Eui-Sub Kim, Junbeom Yoo, Jang-Soo Lee, "Programming Guidelines for FBD Programs in Reactor Protection System Software", Transactions of the Korean Nuclear Society Autumn Meeting, pp 1986-1988, Pyeongchang, Korea, 10.30-10.31, 2014. [Paper, Presentation]
• 이동아, 유준범, 이장수, "원자력 계측제어 소프트웨어의 안전성 분석을 위한 Safety Case 의 Arguments 개발 절차", 2016 한국소프트웨어공학학술대회 (KCSE 2016), pp.476~477, 강원도 보광 휘닉스파크, 2016. [Paper, Presentation] [우수단편논문]
• 김재엽, 이동아, 유준범, "소프트웨어 개발 프로세스를 대상으로 수행하는 추적성 분석의 세부 관계 정의", 2016 한국소프트웨어공학학술대회 (KCSE 2016), pp.409~411, 강원도 보광 휘닉스파크, 2016. [Paper, Presentation]
• 조한석, 이동아, 송지은, 김진영, "STPA를 활용한 전자연동장치의 위험분석 사례", 2018 한국안전학회 추계학술대회, 현대호텔 경주, 2018. [Paper, Presentation]
• Dong-Ah Lee, Junbeom Yoo, "A Model Projection Technique for Compositional Verification using Model Checking", 2020 한국소프트웨어공학학술대회 (KCSE 2020), pp.184~186, 강원도 보광 휘닉스파크, 2020. [Paper, Presentation]

Workshop / Meeting

• Dong-Ah Lee, Jang-Soo Lee, Se-Woo Cheon, and Junbeom Yoo, "Application of System-Theoretic Process Analysis to Engineered Safety Features-Component Control System," Enlarged Halden Programme Group Meeting, Storefjell Resort Hotel, Gol, Norway, 10th–15th March 2013 [Paper, Presentation]
• Dong-Ah Lee, Jang-Soo Lee, Se-Woo Cheon, and Junbeom Yoo, "Application of STPA to Engineered Safety Features of a Nuclear Power Plant", MIT STAMP/STPA Workshop, MIT, Boston, USA, 03.26–28, 2013 [Presentation]

Involved Projects

• SW 요구 및 검증공학 기술연구 센터, 융합 소프트웨어를 위한 요구 및 품질검증 기술 개발, 대학IT연구센터지원사업, 지식경제부, 2009.03. ~ 2012.12.
  • NuFTA 도구 구현
  • 안전성 분석 결과와 테스트 케이스 간의 관계 분석
• 무인비행체SW 연구센터, 무인비행체용 실시간 SW 플랫폼, 대학IT연구센터지원사업, 지식경제부, 2010.03. ~ 2011.12.
  • 무인비행체용 Operational Flight Program 정형 검증
  • 무인비행체용 Operational Flight Program를 위한 검증 절차 수립 및 수행
• 안전 필수 산업분야의‘SW공학 경쟁력 강화를 위한 SW안전성 품질현황 조사’ 용역, 정보통신산업진흥원, 2010.11. ~ 2010.12.
  • 인터넷을 이용한 사례조사
• 안전등급 제어기기 엔지니어링 도구 성능개선 기술개발, 원전기술혁신사업-단기핵심기술, 한국에너지기술평가원, 2010.11. ~ 2013.10.
  • 디자인과 구현물 간의 동일성 검증
• 정형기법 기반 안전등급 계측제어 소프트웨어 평가방법 개발, 주요사업 위탁과제, 한국원자력연구원, 2012.01. ~ 2014.12.
  • 안전성 분석 신기술 적용: STAMP/STPA를 활용한 안전성 분석
• 통합개발환경 확인 및 검증, 창의사업 위탁과제, 한국원자력연구원, 2013.04. ~ 2015.12.
  • FBDEditor 개발
  • FBDtoVerilog for FPGA development 개발
• 통합 모듈형 실시간 운영체제 정형 검증, 한국전자통신연구원, 2016.03. ~ 2017.02.
  • Statemate를 사용한 Qplus-AIR의 최상위 수준 검증
  • SPIN을 사용한 Qplus-AIR의 Communication 검증
• Formal Method 기반 암호 알고리즘 및 보안 프로토콜 검증에 관한 연구, 국가보안기술연구원, 2019.04. ~ 2019.10.
• 무인이동체 보안ㆍ안전성 평가 모델 개발 및 제도 연구, 국가보안기술연구원, 2020.05. ~ 2020.11.
  • STPA를 활용한 드론의 안전성 분석
  • STPA를 활용한 드론의 보안성 분석
• CPS 어플리케이션의 복합적인 안전성 평가 지원을 위한 통합 추적성 분석 기술, 차세대정보컴퓨팅기술개발사업, 2020.04.~2020.12.
  • SoCPSs의 안전성 평가를 위한 체계 수립

Lecture

• Computational Thinking (컴퓨팅적 사고), Konkuk Univ., 2016
• Programming Project (프로그래밍 프로젝트), Konkuk Univ., 2016 [link]
• Introduction to Software Engineering (소프트웨어공학 개론), Konkuk Univ., 2013 [link]

Tools & Software

• NuFTA [link]
• XMLValidator [link]
• pSET2TC6
• FBDtoVerilog [link]
  • Version 1.0 - Verification using VIS, SMV
  • Version 1.1 - Verification using HW-CBMC
  • Version 2.0 - FPGA development
• FBD_FTA [link]
• FBDEditor

Etc.

• Introduction of Dependable Software Laboratory (2010) [link]
• Conference/Journal ranking list for 2008 [link]
• Programming community index [link]
• Conference Calender [link]
• Academic Phrasebank [link]
• High Impact Journals in Computer Science [link]
• CHECK THIS OUT!!