Representative Formal Methods Publications (reverse chronological)

• 2025 – Timed automata to verified Go code
  Soomin Cho, Inhye Kang, and Kim, Jin Hyun. “From timed automata to go: Formally verified code generation and runtime monitoring for cyber-physical systems.” IEEE Access, 13:161729–161749, 2025.   → UPPAAL timed automata 모델로부터 Go 코드와 런타임 모니터를 자동 생성하고, 모델과 구현의 일치성을 형식적으로 보증하는 CPS 코드 생성·모니터링 프레임워크.
• 2021 – Model checking in-vehicle networks
  Kim, Jin Hyun et al. “Model checking resiliency and sustainability of in-vehicle network for real-time authenticity.” Applied Sciences, 11(3), 2021.   → 실시간 인증 프로토콜이 공격 및 고장 상황에서도 시간 제약을 만족하는지 모델 체킹으로 분석하여, 차량 네트워크의 탄력성과 지속가능성을 평가.
• 2016 – Process algebraic timing analysis for automotive software
  Kim, Jin Hyun, Inhye Kang, Sungwon Kang, and Abdeldjalil Boudjadar. “A process algebraic approach to resource-parameterized timing analysis of automotive software architectures.” IEEE Transactions on Industrial Informatics, 12(2):655–671, 2016.   → 자원·시간을 함께 다루는 프로세스 대수(PACoR 계열)로 자동차 소프트웨어 아키텍처를 모델링하고, 자원 파라미터에 따른 응답 시간 및 스케줄 가능성을 형식적으로 분석.
• 2016 – Statistical & exact schedulability of hierarchical systems
  Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim G. Larsen, Marius Mikucionis, Ulrik Nyman, and Arne Skou. “Statistical and exact schedulability analysis of hierarchical scheduling systems.” Science of Computer Programming, 127:103–130, 2016.   → 계층형 스케줄링 시스템을 timed automata로 모델링하고, 정확한 모델 체킹과 통계적 모델 체킹(UPPAAL SMC)을 결합해 스케줄 가능성을 평가.
• 2016 – Optimizing resources in hierarchical scheduling
  Jin Hyun Kim et al. “Optimizing the resource requirements of hierarchical scheduling systems.” SIGBED Review, 13(3):41–48, 2016.   → 형식 분석 결과를 활용하여 계층형 스케줄링 시스템의 CPU 주기·대역폭과 같은 자원 요구량을 최적화하는 방법을 제안.
• 2015 – Formal synthesis of application & platform behaviors
  Kim, Jin Hyun, Inhye Kang, Jin-Young Choi, Insup Lee, and Sungwon Kang. “Formal synthesis of application and platform behaviors of embedded software systems.” Software & Systems Modeling, 2015.   → UML/Statecharts와 프로세스 대수를 기반으로 응용과 플랫폼 행동을 형식적으로 명세하고, 상호 제약을 만족하도록 시스템 행동을 합성(synthesis)하는 방법론.
• 2011 / 2010 – UML + process algebra composite behaviors
  Kim, Jin Hyun et al. “Generating composite behavior of embedded software components based on UML behavioral model and process algebra.” SIGSOFT Software Engineering Notes, 36(1):1–9, 2011. (컨퍼런스 버전: UML&FM 2010)   → UML 행위 모델을 프로세스 대수로 변환하여 컴포넌트 합성 행동을 생성·검증하는 초기 연구로, 이후 형식 합성·분석 프레임워크의 기반을 제공.
• 2010 – Timed & resource-oriented Statecharts (TRS)
  Jin Hyun Kim, Inhye Kang, Jin-Young Choi, and Insup Lee. “Timed and resource-oriented statecharts for embedded software.” IEEE Transactions on Industrial Informatics, 6(4):568–578, 2010.   → 기존 Statecharts를 시간·자원 개념을 포함하는 TRS로 확장하고, 임베디드 소프트웨어의 시·자원 제약을 형식적으로 분석할 수 있는 기반을 제시.
• 2010 – UML behavior models for real-time embedded MDA
  Jin Hyun Kim et al. “UML behavior models of real-time embedded software for model-driven architecture.” Journal of Universal Computer Science, 16(17):2415–2434, 2010.   → 실시간 임베디드 소프트웨어를 위한 UML 행동 모델을 정의하고, 모델 기반 아키텍처(MDA)에서 자동 코드 생성·검증과 연계할 수 있는 설계 흐름을 제안.
• 2008 – Resource-oriented design framework
  Jin Hyun Kim, Jae-Hwan Sim, and Jin-Young Choi. “Resource-oriented design framework for embedded system components.” Electronic Notes in Theoretical Computer Science, 215:171–189, 2008.   → 임베디드 컴포넌트를 자원 중심으로 모델링하는 이론적 프레임워크를 제시하며, 이후 자원 기반 프로세스 대수 및 TRS 연구의 기반을 제공.
• 2006 – Formal specification & verification of PLC
  Jin Hyun Kim, Na Young Lee, and Jin-Young Choi. “Formal specification and verification of PLC for certification.” SIGBED Review, 3(4), 2006.   → 원전·산업용 PLC 제어 로직을 형식 명세 언어로 기술하고 모델 체킹을 통해 인증용 검증 근거를 생성한 사례 연구.
• 2003 – Modeling & analysis framework for real-time OS
  Jin Hyun Kim and Jin-Young Choi. “A framework for modeling and analysis of real-time system operating system.” In ATVA, 2003.   → 실시간 운영체제를 위한 형식 모델링·분석 프레임워크를 제시한 초기 연구로, 이후 자원 기반 실시간 OS/스케줄링 분석의 출발점이 되는 작업.