왜 안전 규격은 형식기법을 요구하는가

“형식기법”이라는 말을 처음 들었을 때 장비 엔지니어의 반응은 대체로 같습니다.

“수학 얘기 아닙니까. 우리랑은 상관없습니다”

무리도 아닙니다. 기호가 늘어서고 증명이라는 단어가 나오니, 장비를 돌리는 사람의 일상에서는 멀리 떨어진 이야기로 보입니다. 학회에서 발표되는 종류의 것이고, 월요일 아침에 현장 시운전하는 장비와는 접점이 없다. 그렇게 읽는 것이 자연스럽습니다.

다만 한 가지 걸리는 것이 있습니다. 그 “상관없는 이야기”를 자사 책장에 꽂혀 있는 안전 규격 쪽에서 이름을 대며 지목하고 있다는 사실입니다.

규격은 이미 써 놓았습니다

분야별로 이렇게 되어 있습니다.

규격	영역	형식기법의 위치
IEC 61508	기능 안전(일반)	최고 안전 등급 SIL 4에서 형식기법을 highly recommended
EN 50128	철도	SIL 3·4에서 강력히 권장
ISO 26262	자동차	권장
DO-178C	항공	형식기법 적용 지침 DO-333을 별도로 규정

한 줄씩 읽으면 권장 사항 목록으로 보입니다. 나란히 놓고 읽으면 다른 것이 보입니다.

기능 안전 일반 규격, 철도, 자동차, 항공 —— 서로 독립적으로 만들어졌고, 각기 다른 위원회가 각기 다른 사고의 역사를 짊어지고 쓴 것들입니다. 그 넷이 같은 기술에 손을 뻗고 있습니다.

특히 DO-178C 줄은 잠깐 멈춰 볼 가치가 있습니다. 항공은 형식기법을 언급하는 데 그치지 않았습니다. 어떻게 적용할지를 별책으로 써냈습니다 —— 그것이 DO-333입니다.

아무도 쓰지 않는 것을 위해 보충 문서를 쓰지는 않습니다. 적용 지침이 필요한 것은, 실제로 적용하는 사람이 있고 그 적용 방식에 따라 인증의 가부가 갈리기 때문입니다. 언급과 별책 사이에는 거리가 있습니다.

왜 따로 만들어진 규격들이 같은 결론에 도달했는가

이유는 이 연재에서 계속 써 온 한 문장과 같습니다.

일찍 발견할수록 후공정의 비용이 크게 내려간다.

규격이 형식기법에 다다른 것은 그것이 이론으로서 아름답기 때문이 아닙니다. 안전에 관련된 오류를 늦게 발견하는 일이 단순히 수지가 맞지 않기 때문입니다. 현장에서 발견되면 재작업. 양산에서 발견되면 리콜. 인증을 통과한 뒤에 발견되면 재제출.

그리고 하나 더 있습니다. 어떤 위험도를 넘어서면 테스트만으로는 “그런 오류는 없다”고 단언할 수 없게 됩니다.

이것은 규격을 쓴 사람들이 심술궂어서가 아닙니다. 동시에 움직이는 것이 늘어날수록 일어날 수 있는 순서는 조합으로 늘어납니다. 어느 수준부터는 전부 시험했다고 주장하는 것 자체가 물리적으로 불가능해집니다. SIL 4란 거기까지 와 버렸다는 뜻입니다.

인증에서 묻고 있는 것은 버그의 개수가 아닙니다

여기가 가장 중요한 지점이라고 생각합니다.

인증이나 품질 감사에서 하는 일은 오류를 고치는 것만이 아닙니다. 평가자를 상대로 주장을 세우는 일입니다. 이 장비는 안전하다고 말하고, 그 근거를 제시합니다. 상대가 보는 것은 근거의 질입니다.

두 문장을 나란히 놓아 보십시오.

“테스트했습니다만, 그 현상은 발생하지 않았습니다”

“그 상태에는 구조적으로 도달할 수 없음을 보였습니다”

문장으로는 비슷합니다. 내용은 전혀 다릅니다. 앞의 문장이 보여주는 것은 관측되지 않았다는 사실입니다. 뒤의 문장이 보여주는 것은 존재하지 않는다는 사실입니다.

“발생하지 않았습니다”는 관측의 부재이고, “도달할 수 없습니다”는 사건의 부재입니다. 둘의 차이는 시험한 횟수로는 메워지지 않습니다.

평가자는 이 차이를 압니다. 고객사의 품질 감사도 압니다. “몇 번 테스트했습니까”라는 질문을 받고 있는 자리는, 사실 “당신의 주장은 둘 중 어느 쪽입니까”라는 질문을 받고 있는 자리입니다.

어려운 절반은 이미 끝나 있습니다

형식기법이라고 하면 맨바닥에서 새로운 작업이 늘어나는 것처럼 들립니다. 여기는 오해입니다.

귀사는 이미 리스크 평가를 하고 있습니다. HAZOP을 하고, 위험 사건을 뽑아내고, 목록으로 만들어 두었습니다. 안전 요구 사양으로 옮겨 놓았습니다. 인증을 위해 이미 하고 있을 것입니다.

그 목록을 다시 한번 보십시오.

두 축이 동시에 위험 영역에 들어간다
도어가 열린 상태에서 반송이 움직인다
비상 정지에서 어떻게 해도 복귀할 수 없는 상태가 남는다

이것은 서류를 위한 서류가 아닙니다. 형식 검증이 입력으로 받아먹는 것, 바로 그것입니다. 위험 시나리오 하나하나가 “이 상태에 도달 가능한가”라는 질문으로 그대로 변환됩니다. 그리고 도달 불가능함을 보이는 것이 형식기법이 하는 일입니다.

즉, 어려운 절반은 이미 끝나 있습니다. 무엇이 위험한지 알고 있는 것은 규격도 도구도 아닙니다. 그 장비를 만드는 사람입니다. 모자란 것은 그 목록을 “일어나지 않았습니다”에서 “일어날 수 없습니다”로 바꾸는 수단 쪽입니다.

솔직하게 적어 둡니다

여기까지 읽고 “우리도 서둘러야겠다”고 생각한 분이 있다면 일단 멈춰 주십시오.

귀사의 장비는 아마 SIL 4가 아닙니다. DO-178C 아래에 있지도 않습니다. 일반적인 공장 자동화 장비를 만들고 있다면, 지금 형식기법을 의무화하고 있는 규격은 없습니다. 이 글은 없는 의무를 있는 것처럼 보이게 하려고 쓴 것이 아닙니다.

그러면 규격 이야기는 무엇을 위해 한 것인가.

규격은 따라야 할 명령이 아니라, 어려움이 어디에 있는지를 알려주는 신호로 읽을 가치가 있습니다. 네 개의 규격이 독립적으로 같은 곳에 손을 뻗었다는 사실은 그 기술에 대한 정보입니다. 그것이 자신에게 의무화되어 있는지 여부와는 별개의 정보입니다.

틀리는 것이 허용되지 않았던 산업 —— 철도, 항공, 자동차의 안전 기구 —— 은 비용을 감수하고 여기에 손을 뻗었습니다. 그들이 겁이 많아서가 아닙니다. 그들이 있는 곳에서는 늦게 발견하는 것의 가격이 먼저 드러났을 뿐입니다. 장비 업계에서 그 가격이 싸다는 뜻은 아닙니다. 청구서가 도착하는 방식이 다를 뿐입니다.

하나 더, 실무적인 관찰을 적어 둡니다. 인증의 압력은 대개 규제 당국보다 먼저 고객사와 수출 대상국에서 옵니다. 어느 날 들어온 견적 요청 사양서에 안전 등급이 적혀 있습니다. 어느 나라에 납품하려고 보니 요구 수준이 다릅니다. 규제가 바뀌기를 기다리고 있으면 그 시점에는 이미 늦다, 는 순서가 되기 쉽습니다.

지금은 의무가 아니다, 는 맞습니다. 앞으로도 계속 상관없다, 는 또 다른 이야기입니다.

다음에 읽을 글

규격이 권장하고 있다는 것은 알겠다. 그러면 실제로 쓰고 있는 곳은 어디인가 —— 누가 실제로 쓰고 있는가에 공개된 사례와, 보급이 어디까지 진행되지 않았는지를 나란히 놓았습니다.

“테스트했습니다”와 “보였습니다”의 차이가 기술로서 무엇인지. 그것은 테스트와 형식기법은 무엇이 다른가에서 다룹니다.