[연구의 필요성]
-Programmable Logic Controller (PLC)는 선박, 공장, 로봇 등 산업 현장을 제어하기 위해 널리 사용되는 컴퓨터 시스템으로, 물리적인 외부 환경과 상호작용하기 때문에 오류 발생시 사고로 이어져 큰 피해를 발생시킬 수 있으므로 높은 안전성이 요구됨.
-PLC 소프트웨어의 높은 신뢰성을 보장하기 위해서, 기존에 개발자가 수동으로 코드를 분석하거나 테스트를 수행하는 전통적인 방법을 벗어나, 안전성 요구사항을 자동으로 분석하여 엄밀하게 검증하는 기술의 필요성이 요구되고 있음.
-기존의 PLC를 자동으로 검증하기 위한 기술들은 대부분 단일 작업에만 초점을 맞추어, 실제 PLC 시스템에 사용되는 선점형 멀티태스킹을 통하여 발생하는 복잡한 경우들을 엄밀하게 분석하지 못하는 문제로 실제 시스템에 적용이 제한됨.

[포스텍이 가진 고유의 기술]
-논리적으로 기술된 안전성 요구사항을 바탕으로, PLC 소프트웨어의 행위를 자동으로 분석하기 위한 이론과 알고리즘을 개발하고, 이를 바탕으로 PLC에서 가장 널리 쓰이는 프로그래밍 언어인 Structured Text(ST)를 검증하는 STbmc 도구를 개발함.
-선점형 멀티태스킹과 실시간 제약조건을 고려한 PLC ST 언어의 수학적인 의미구조를 엄밀하게 제안하였으며, 요약해석 이론에 기반하여 연속적인 시간 흐름에 따른 무한히 많은 행위들을 유한한 동등한 행위들로 요약하는 이론을 개발하였음.
-선점형 멀티태스킹을 고려하는 복잡한 PLC 소프트웨어의 알고리즘적인 분석의 성능을 높이기 위하여, PLC ST 언어의 의미구조에 기반하는 상태기반 축소 기술을 개발하고, 이를 바탕으로 효과적인 모델검증(Model checking) 알고리즘을 개발하였음.

[연구의 의미]
-기존에 거의 연구되지 않았던 선점형 멀티태스킹을 고려한 PLC ST 프로그래밍 언어의 의미구조를 최초로 제시하였음. PLC ST 소프트웨어의 정적분석, 테스팅, 모델검증 등 향후 다양한 연구에서 본 연구에서 제안된 의미구조가 사용될 것으로 예상됨.
-단순한 이론 및 알고리즘 뿐만 아니라, 실제 PLC 소프트웨어 개발에 활용될 수 있는 STbmc 도구를 개발함. 해당 도구는 유럽 입자 물리학 연구소(CERN)에서 개발하여 사용하고 있는 PLC 언어 검증 도구(PLCVerif)와 비교하여 더 우수한 성능을 보임.
-산업 현장에서 널리 사용되고 있는 PLC 소프트웨어의 안전성과 신뢰성을 향상시킬 수 있는 기술을 개발함으로써, 소프트웨어 오류로 인한 인명 및 재산 피해를 미연에 방지하고 소프트웨어 오류가 야기하는 사회적 비용 및 기업 손실 방지.

[연구결과의 진행 상태 및 향후 계획]
-PLC ST 언어의 선점형 멀티태스킹 의미구조에 대한 연구 결과는 정형기법 분야에서 가장 저명한 국제학술회의인 International Symposium on Formal Methods(FM)에 2024년에 발표되었음.
-후속 연구로, PLC에 의해 제어되는 외부 물리 모델의 행위를 동시에 고려하여 검증을 수행할 수 있는 기술을 연구하고 있으며, 검증 도구인 STbmc를 오픈소스로 공개하고 이를 다양한 시스템의 검증에 적용하는 사례연구를 진행하고 있음.

[성과와 관련된 실적]
-Jaeseo Lee and Kyungmin Bae. Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption. International Symposium on Formal Methods (FM),
-Jaeseo Lee, Sangki Kim, and Kyungmin Bae. Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT. ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2022.

[성과와 관련된 이미지]

그림 PLC 소프트웨어 자동검증 기술 개요

그림 산업현장에 설치된 PLC 머신