보잉 737 맥스는 2018년과 2019년 두 차례 추락 사고로 346명의 목숨을 앗아가면서 한국을 비롯한 전 세계 40여개 국에서 운항이 중단됐다. 사고 원인으로는 비행기의 급강하를 막아주는 소프트웨어인 조종특성향상시스템(MCAS)의 결함이 지목됐다. 이는 최근 소프트웨어 활용이 급격히 늘면서 소프트웨어가 일으키는 사고 또한 심각한 피해를 일으킬 수 있다는 예로 지목된다.

배경민 컴퓨터공학과 교수가 이끄는 소프트웨어 검증 연구실은 소프트웨어 오류를 방지하고 신뢰성과 안전성을 높이는 기술과 이론, 알고리즘, 도구를 개발하고 있다. 지금까지는 소프트웨어의 동작을 시험하기 위해서 개발자가 수작업으로 실행 결과가 올바른지를 확인하는 방법이 활용돼왔다. 그러나 점차 소프트웨어가 복잡해지고 개발주기도 빨라지면서 사람의 손으로는 한계가 생겼다.

연구실은 자동차나 항공기 같은 물리적인 환경에서 한 치의 오차도 없이 동작해야 하는 소프트웨어를 검증하는 ‘사이버물리시스템’ 검증 기술을 개발중이다. 사이버물리시스템 소프트웨어는 시속 100km로 달리는 자동차가 주변 위험을 인지하고 급히 브레이크를 밟는 것과 같은 시시각각 주변 환경이 변하는 상황에서 동작한다. 기존 소프트웨어 검증기술은 소프트웨어의 논리적 오류만 찾으면 되지만 주변 상황에 따라 달라지는 복잡한 물리적 요구사항은 검증할 방법이 없었다.

연구실은 사이버물리시스템이 가지는 다양한 상황을 논리적 언어로 표현하여 엄밀하게 검증하는 이론을 세계 최초로 제안하고 이론에 기반한 알고리즘과 도구를 개발했다. 소프트웨어를 통해 바뀌는 물리적 환경을 구축해 디지털뿐 아니라 물리 시스템에서도 요구사항을 검증하는 것이다. 연구팀은 알고리즘이 분석해야 하는 경우의 수가 기하급수적으로 늘어나는 ‘상태폭발문제’를 추론을 통해 빠르게 알아낼 수 있는 알고리즘도 개발하고 있다.

자동차나 항공, 의료, 금융, 전력 등 각종 기간 시스템에 적용되는 소프트웨어가 검증된 소프트웨어이냐 아니냐는 앞으로 소프트웨어 선진국을 판가름하는 핵심 요소가 될 것으로 꼽힌다. 미국이나 유럽에서는 검증 도구를 개발해 학회에서 발표하는 등 이미 앞서나가고 있다. 배 교수는 “검증된 소프트웨어를 개발하는 기술을 세계적으로 선도해 안전한 인프라 구축에 기여할 것”이라고 말했다.