[연구의 필요성]

프로그래머블 로직 컨트롤러(PLC)는 선박, 발전소, 공장 자동화 설비 등 다양한 산업 현장에서 사용되는 산업 제어용 컴퓨터이다. 산업 현장에 직접 투입되는 특성 상 작은 오류도 대형 사고로 이어질 수 있어 매우 높은 수준의 안정성과 신뢰성이 요구된다. 기존의 기술은 개별 PLC 프로그램에 초점을 맞추어, 제어기들이 서로 통신하며 물리 환경과 상호작용하는 실제 산업 시스템의 복잡성을 고려하지 못하는 한계가 있었다. 이에 따라 프로그램·통신·물리환경을 통합적으로 고려한 새로운 검증 기술이 필요하다.

[포스텍이 가진 고유의 기술]

본 연구진은 PLC 프로그램의 실행, PLC 사이의 통신, 그리고 물리 환경의 연속적인 변화를 하나의 통합된 수학적 의미구조(정형명세)로 표현하는 기술을 개발하였다. 이를 통해 실제 산업 현장의 PLC 시스템을 보다 현실에 가깝게 모델링할 수 있다. 물리적인 환경과 통신을 고려하는 PLC 정형명세에 대한 검증 알고리즘은 매우 방대한 상태 공간을 생성하는 문제가 있으나, 본 연구진은 PLC의 실행 특성과 통신 구조를 활용한 상태 공간 축소 기법을 함께 적용하여, 검증 효율성을 크게 향상시켰다.

[연구의 의미]

본 연구는 PLC 프로그램, 네트워크 통신, 물리 환경의 연속적 동작을 하나의 통합된 의미구조로 동시에 다룬 최초 수준의 연구로, 기존에 분리되어 다루어지던 산업 제어 시스템 분석의 한계를 근본적으로 극복하였다. 이러한 통합 모델에서 필연적으로 발생하는 검증 복잡도 문제를 해결하기 위해, PLC 실행 구조와 통신 특성을 활용한 상태 공간 축소 기법을 함께 제안함으로써, 이론적 정합성과 실용적 분석 가능성을 동시에 달성하였다. 실제 산업 현장에서 발생하는 복합적인 상호작용을 정밀하게 분석할 수 있는 새로운 PLC 검증 패러다임을 제시하였으며, 향후 다양한 안전 필수 시스템의 신뢰성 검증에 폭넓게 활용될 수 있는 기반을 마련하였다.

[연구결과의 진행 상태 및 향후 계획]

후속 연구로, 현재 제안한 통합 의미구조를 다중작업(multitasking) PLC 시스템으로 확장하고, 이러한 확장에 따라 증가하는 검증 복잡도를 완화하기 위해 다중작업 PLC 환경에 적합한 상태 공간 축소 기법을 고도화하는 연구를 수행하고 있다.

[성과와 관련된 실적]

Jaeseo Lee and Kyungmin Bae. Formal Analysis of Networked PLC Controllers Interacting with Physical Environments. Static Analysis Symposium (SAS), 2025.

[성과와 관련된 이미지]

그림1.  대표적인 PLC 벤치마크 모델 SWaT의 도식

그림2.  PLC 자체 언어로 명세된 복잡한 통신 행동