일본산업뉴스요약

Nikkei X-TECH_2020.9.18

수학적으로 결함 제로의 소프트 개발
도요타 산하의 JTEKT와 NVIDIA가 주목

차량탑재 소프트의 결함(버그)을 제로로 하는 개발 방법이 주목을 받고 있다. 자율주행을 배경으로 소프트의 안전성이나 보안을 지금까지 이상으로 높일 필요성이 등장했기 때문이다. 도요타 산하에서 전동파워스티어링(EPS)를 전개하는 제이텍트(JTEKT)가 양산에 도입할 생각이다. 또한 자율주행용 차량탑재 SoC(System on Chip)를 전개하는 미국 NVIDIA도 같은 방법을 검토하고 있다.

제이텍트나 NVIDIA가 검토하고 있는 것은 소프트에 결함이 없다는 것을 수학적으로 증명하는 ‘정리 증명(형식 방법의 일종)’이다. 자율주행이나 Steer By Wire(SBW)의 실용화에 따라 차량탑재 소프트의 안전 요구는 급격하게 높아지고 있다. 지금까지는 시스템의 주기능에 고장이 발생했을 경우에 안전기구를 통해 시스템을 정지하면 됐었다. 그러나 자율주행이나 SBW에서는 시스템을 정지하면 오히려 위험하기 때문에 안전기구에 의해 최저한의 기능(백업 기능)을 계속할 필요가 있다.

제이텍트 스티어링사업본부 요네키(米木) 씨는 “그러나 이러한 안전기구의 실장이 곤란한 경우도 있다”라고 말한다. 일반적으로 안전기구에는 주기능과는 다른 실장 형태의 소프트를 내장한다. 그러나 EPS의 경우는 주기능도 안전기구도, 같은 입력에 대해 같은 출력을 돌려줄 필요가 있어 소프트의 실장 형태를 바꾸는 것이 어렵다. 이 때문에 안전기구가 없어도 주기능만으로 문제가 없다는 것을 증명하는 방법을 제이텍트는 찾고 있었다.

통상 차량탑재 소프트의 안전성은 테스트 공정에서 검증한다. 그러나 결함이 없는 것을 증명하는 것은 어렵다. 테스트 조건은 무수하게 많다. 아무리 포괄성을 높인다고 해도 결함이 없다고 단정하기는 어렵다. 그 때문에 최종적으로 안전한지 여부는 고객이 판단하게 된다. 이에 대해 정리 증명에서는 수학적으로 소프트의 결함이 제로라는 것을 증명할 수 있다. “누구나가 납득할 수 있는 판단 재료로서 사용할 수 있다”(요네키 씨).

-- SPARK 언어를 선택 --
툴에는 미국 AdaCore가 제공하는 ‘SPARK Pro’를 사용했다. 현재는 도입 단계이기 때문에 C언어로 쓰인 소스 코드를 정리 증명 언어 ‘SPARK’로 변환해 검증하고 있다. 오류가 없다는 것을 확인하면 다시 C언어의 소스 코드로 변환한다. 장기적으로는 소프트를 신규로 개발할 때 처음부터 SPARK로 기술하고, 정리 증명을 끝낸 후에 C언어로 변환하는 것을 상정한다.

사용 방법은 ‘코드 검토(code review)’에 가깝다고 한다. 그러나 언어가 C언어가 아니라 SPARK가 된다. SPARK에서는 프로그램에 더해 검증하고 싶은 속성(사양 상의 입출력 범위 등의 조건)을 기술할 수 있다. 검증 툴을 작동시키면 프로그램이 틀렸는지 혹은 사양이 틀렸는지 그 자리에서 바로 알 수 있다. 코드 검토를 기계로 대체한 것이라고도 할 수 있다.

예를 들면 프로그램은 과거의 노하우를 바탕으로 오류가 없다고 알고 있는데도 사양과 프로그램에 오류가 발견됐을 경우, “사양에 누락이 있었다는 것을 알게 된다. 이러한 오류는 테스트 공정에서도 발견할 수 있을 가능성이 있지만 소프트 기술자가 프로그램을 쓰면서 직접 체크할 수 있다면 결과적으로 빨리 일을 진행할 수 있다”(요네키 씨).

제이텍트가 과거에 전개한 제품에서는 테스트 공정에서 발견된 오류의 대부분은 소프트의 사양이나 실장(프로그램) 실수에 기인했었다. 오류의 2대 원인인 사양과 실장 실수를 개발 단계에서 줄이는 것은 큰 이점이라고 할 수 있다.

-- 만능이 아니다 --
그러나 이 방법은 만능이 아니다. 정리 증명을 단체(單體) 테스트의 대체 수단으로서 어느 정도 사용할 수 있다는 것은 확인할 수 있었다. 그러나 SPARK로 발견할 수 있는 오류가, 기존 툴로도 발견할 수 있는지 여부를 비교 검토할 필요가 있다. 그 작업을 현재 추진하고 있다고 한다.

그리고 최대 과제는 정리 증명을 적용할 수 있는 프로그램이 한정적이라는 것이다. “정리 증명의 근간이 된 호어 논리(Hoare Logic)와 친화성이 높은 프로그램이 아니면 적용하기 어렵다”(요네키 씨). 한편으로 피드백 제어처럼 직전 상태에 의존해 출력이 바뀌는 프로그램의 경우는 입출력 범위의 기술이 어려워 적용하기 어렵다고 한다. 프로그램 별로 친화성을 확인할 필요가 있다.

제이텍트에서는 우선은 하드웨어와 직접 교류하는 단말의 소프트 부품이나 기본적인 제어 프로그램 등에 사용할 생각이다. 이들 소프트는 그다지 복잡한 제어는 하지 않지만 오류가 발생하면 안전 상의 영향이 크다.

정리 증명을 적용하는 소프트의 규모(코드 행수)는 EPS의 시스템 전체에서 보면 수 % 이하로 작다. 그래도 그 부분은 결함이 없다고 단정하는 것이 중요하다고 한다. 소규모 단말의 소프트 부품이 무결함이라는 것을 먼저 증명하고, 그 후에 실현하고 싶은 기능을 축적함으로써 시스템 전체의 안전성을 높일 생각이다.

NVIDIA도 AdaCore의 SPARK 언어나, SPARK의 근간이 된 ‘Ada 언어’에 주목하고 있다. 보안이 중요한 일부 펌웨어에 취약성이 있으면 사이버 공격의 표적이 된다. 정리 증명을 통해 취약성을 배제할 수 있다면 보안 향상의 가능성이 있다.

 -- 끝 --

Copyright © 2020 [Nikkei XTECH] / Nikkei Business Publications, Inc. All rights reserved.