새로운 기법 이야기를 들었을 때, 장비 업계 사람이 가장 먼저 알고 싶어 하는 것은 효과가 아닙니다.
“그래서, 어디가 쓰고 있습니까”
이 질문은 의심이 많아서 나오는 것이 아닙니다. 장비는 십 년 넘게 돌아갑니다. 납품한 곳의 생산 라인이 멈추면 그 책임은 자신들에게 돌아옵니다. 실적 없는 것을 고객사 장비에 실을 수 없다는 것은 신중함이 아니라 업무상 당연한 전제입니다.
그래서 그 질문에 먼저 답하겠습니다. 효과 이야기는 그다음에 하겠습니다.
AWS는 2011년부터 쓰고 있습니다
Amazon Web Services는 2011년부터 실제 프로덕션 시스템에 TLA+라는 형식기법을 쓰고 있습니다. 연구 부서의 실험이 아닙니다. 가동 중인 서비스의 설계에 적용했고, 사내에서는 경영진이 적극적으로 확산시켜 왔습니다. 담당했던 엔지니어들이 직접 “Use of Formal Methods at Amazon Web Services”라는 논문으로 정리했고, 이 논문은 TLA+의 작성자인 Lamport의 사이트에 공개되어 있습니다.
왜 그들이 거기까지 하는지는 장비 하는 사람에게는 이해하기 쉬운 이야기입니다. AWS의 사업은 분산 시스템이 올바르게 동작한다는 것 위에 전부 얹혀 있습니다. 그리고 분산 시스템에서 비싼 오류는 코드를 잘못 쓴 것이 아닙니다. 여러 개가 동시에 움직였을 때만 나타나는, 드문 순서입니다.
동시에 움직이는 것들. 드물게만 나타나는 순서. 테스트로 재현할 수 없는 현상 —— 장비 엔지니어가 “가끔 멈춥니다”라고 부르는 것과 같은 종류의 오류입니다.
Airbus는 단위 테스트를 대체할 수 있는지 조사하고 있습니다
Airbus는 형식기법이 단위 테스트를 대체할 수 있는지를 검토하고 있습니다.
이 문장의 무게는 잠깐 멈춰 볼 가치가 있습니다. 그들이 조사하고 있는 것은 “테스트의 보조로 쓸 수 있는가”가 아닙니다. “테스트 대신 세울 수 있는가”입니다. 항공기의 단위 테스트는 하고 싶으면 하는 작업이 아니라, 인증상 반드시 해야 하는 작업입니다. 그것을 다른 수단으로 대체할 수 있는지를 진지하게 검토 대상으로 삼고 있습니다.
오해가 없도록 적어 두면, 이것은 검토 단계의 이야기이지 대체가 완료됐다는 이야기가 아닙니다. 다만 검토 대상이 될 수 있는 데까지는 와 있다는 뜻입니다. 의무화된 검증 활동의 대체 후보로 이름이 오르는 기법은 그리 많지 않습니다.
CERN과 GSI는 PLC 검증을 “서비스”로 내놓았습니다
장비 업계에 가장 가까운 선례는 이것이라고 생각합니다.
CERN과 GSI는 “Formal Verification of PLCs as a Service”라는 활동을 공개하고 있습니다. 읽어야 할 곳이 두 군데 있습니다.
하나는 PLC입니다. 웹 서버도, 항공기의 제어 컴퓨터도 아닙니다. 공장의 장비를 돌리고 있는 것과 똑같은, 산업용 제어 기기입니다. 형식기법이 클라우드나 항공 안에서만 성립하는 이야기라면 우리와는 상관이 없습니다. 그런데 이것은 산업 제어 그 자체를 겨냥하고 있습니다.
다른 하나는 as a Service —— “서비스로서”라는 부분입니다. 즉, PLC를 작성하는 팀 쪽에 형식기법 전문가를 둔다는 전제를 취하지 않았습니다. 전문가는 바깥에 있고, 검증만 바깥에서 제공됩니다. 장비를 만드는 사람은 계속 장비를 만듭니다.
사내에 형식기법 전문가를 한 명 채용해서 키운다는 이야기라면, 중견 장비 제조사에게는 현실적이지 않습니다. 밖에서 검증을 받아 오는 형태라면 이야기가 달라집니다. 중견 장비 제조사가 실제로 살 수 있는 형태에 가장 가까운 공개 사례입니다. 저희가 만들려고 하는 것도 이 형태입니다.
세 사례에 공통된 것
클라우드 인프라, 항공기, 가속기 제어. 나란히 놓으면 서로 아무 관계도 없어 보입니다. 장비 업계와도 관계가 없어 보입니다.
공통점은 하나입니다. 셋 다 여러 개가 동시에 움직이는 시스템이고, 셋 다 비싼 오류가 테스트로 재현할 수 없는 쪽에 있다는 것입니다.
그래서 그들은 테스트를 두껍게 하는 방향이 아니라, 설계 자체를 조사하는 방향에 돈을 냈습니다. 순서의 조합을 사람이 다 셀 수 없다는 것을 이른 단계에서 인정했기 때문입니다.
자동화 장비는 이 가족의 일원입니다. 축이 있고, 반송이 있고, 상위 제어가 있고, 인터록이 있고, 그것들이 동시에 움직입니다. 드문 순서로 맞물렸을 때만 멈춥니다. 구조는 같습니다. 다만 아직 그렇게 불리지 않았을 뿐입니다.
솔직하게 적어 둡니다 —— 보급되지 않았습니다
여기까지 읽으면 업계 표준이 되어 가는 기술 이야기처럼 들릴지도 모릅니다. 그렇지 않습니다.
형식기법의 산업계 채택은 지금도 제한적이고 니치합니다. 이것은 반대편의 평가가 아닙니다. AWS 자신이 그렇게 말하고 있습니다. 십 년 넘게 써 온 당사자가, 널리 퍼지지는 않았다고 말합니다.
그러면 효과가 없어서 퍼지지 않는 것인가. 전문가 130명을 대상으로 한 조사에서는 채택의 최대 장벽으로 **71.5%가 “엔지니어의 교육 부족”**을 꼽았습니다. 1위는 “기법이 유효한지 의심스럽다”가 아닙니다. 쓸 수 있는 사람이 없다, 입니다.
즉, 막혀 있는 지점은 기술 쪽이 아니라 사람 쪽입니다.
기술은 이미 실증되었습니다. 보급은 아직입니다.
이것이 세계의 실제 상태입니다. 틀리는 것이 허용되지 않는 조직은 십 년도 더 전부터 써 왔습니다. 그 외에는 손대지 않았습니다. “다들 하고 있습니다”도 아니고, “이것이 미래입니다”도 아닙니다. 둘 중 어느 쪽도 아니라는 사실이 지금 손에 있는 답입니다.
그래서 “아직 보급되지 않았으니 위험하다”도, “이미 업계 표준이니 서둘러라”도 둘 다 상황을 잘못 읽은 것입니다. 올바른 독법은 이렇습니다 —— 효과가 있다는 것은 이미 밝혀져 있다. 남은 것은 우리가 쓸 수 있게 되는 길이 있는지 여부뿐이다.
그리고 CERN과 GSI의 사례가 보여주는 것은, 그 길이 “사내에서 전문가를 키운다” 하나뿐인 것은 아니라는 사실입니다.
다음에 읽을 글
형식기법을 요구하고 있는 것은 앞서가는 기업들만이 아닙니다. 안전 규격 자체가 조건부로 이것을 요구하고 있습니다. 그 사정은 왜 안전 규격은 형식기법을 요구하는가에서 다룹니다.
애초에 왜 장비 소프트웨어는 테스트에만 의존할 수 없는가. 그 구조는 왜 장비 소프트웨어는 V자 모델의 오른쪽 절반을 실행할 수 없는가에 있습니다.