테스트와 형식기법은 무엇이 다른가

출하 전 테스트는 전부 통과했습니다. 절차서 항목에 불합격은 하나도 없습니다. 장비는 공장에서 2주 동안 문제없이 돌았습니다.

그리고 현장에서 사흘째에 멈췄습니다.

날아가서 같은 절차를 수십 번 되짚습니다. 멈추지 않습니다. 로그에는 멈춘 전후만 남아 있습니다. 가지고 돌아와서 재현을 시도합니다. 나오지 않습니다. 그래도 대책서는 써야 합니다.

이 버그는 테스트를 못해서 새어 나간 것이 아닙니다. 테스트라는 방법으로는 구조적으로 닿지 않는 자리에 있습니다.

시험해 본 범위와, 일어날 수 있는 전부

먼저 가장 오해받기 쉬운 부분을 적어 두겠습니다.

형식기법은 테스트를 대체하지 않습니다.

형식기법이 확인하는 것은 설계입니다. 조립된 장비가 아닙니다. 배선이 도면대로인지, 모터가 지령대로의 시간에 멈추는지, 센서가 사양대로의 임계값에서 반응하는지 —— 이것들은 테스트로만 알 수 있습니다. 모델이 추상화하면서 버린 부분은 전부 테스트의 몫입니다.

둘은 서로 다른 질문에 답하고 있습니다. 테스트는 “이 장비는 움직이는가”를 확인합니다. 형식기법은 “이 설계는 깨질 수 있는가”를 확인합니다. 어느 한쪽만으로 충분한 경우는 없습니다.

그 위에서, 차이는 한 줄로 쓸 수 있습니다.

테스트는 “시험해 본 범위”를 확인합니다. 형식기법은 “일어날 수 있는 모든 상태”를 확인합니다.

이 차이가 효과를 내는 것은 버그가 범위 바깥에 있을 때뿐입니다. 그리고 장비 소프트웨어에서 가장 비싸게 먹히는 버그는 대개 범위 바깥에 있습니다.

두 개의 축과 하나의 인터록

교과서적인 예를 하나 놓겠습니다.

반송축과 승강축이 있고, 동작 범위가 일부 겹칩니다. 겹치는 부분을 공유 영역이라고 부릅니다. 안전 조건은 하나입니다.

공유 영역에 들어갈 수 있는 것은 언제나 둘 중 하나뿐.

설계는 이렇습니다. 각 축은 진입 전에 영역의 상태를 읽습니다. 비어 있으면 진입하고, 진입한 것을 점유 센서가 검지해서 점유 플래그가 섭니다. 다른 쪽은 그 플래그를 보고 기다립니다.

읽어 보면 맞아 보입니다. 실제로 대부분의 경우 제대로 동작합니다.

문제는 이 순서입니다.

1. 반송축: 공유 영역의 상태를 읽음 → 비어 있음
2. 승강축: 공유 영역의 상태를 읽음 → 비어 있음   ← 반송축은 아직 진입하지 않음
3. 반송축: 진입 개시 → 점유 센서 검지 → 점유 플래그=점유
4. 승강축: 스텝 2에서 "비어 있음"을 읽었으므로 그대로 진입 개시
5. 두 축 모두 공유 영역 안

창은 스텝 1과 3 사이에 있습니다. 상태를 읽은 뒤부터 점유 플래그가 설 때까지. 설계도 위에서는 “확인하고, 들어간다”는 하나의 동작으로 보였습니다. 실제로는 확인과 점유 확정이 별개의 사건이고, 그 사이로 다른 쪽의 확인이 끼어들 수 있습니다.

테스트를 늘려도 여기에는 수렴하지 않는다

이 설계에서 테스트는 통과합니다. 몇 번이든 통과합니다.

절차서를 따라 움직이는 한, 두 번의 확인이 같은 창에 떨어지는 일은 거의 일어나지 않습니다. 창의 폭은 제어 주기 몇 회분이고, 테스트 때의 지령은 스크립트나 조작자가 순서대로 냅니다. 노리고 만들지 않는 한 걸리지 않습니다.

여기가 핵심입니다. 걸리지 않는 테스트를 천 번 돌려도, 걸리지 않는 회차가 천 번 이어질 뿐입니다.

발생 확률이 낮다는 것이 “횟수를 늘리면 언젠가 걸린다”를 뜻하지는 않습니다. 걸리는지 아닌지는 테스트 환경이 그 창을 열 수 있는지에 달려 있습니다. 상위의 주기가 현장에서 바뀝니다. 통신이 한 번 늦습니다. 리트라이가 들어갑니다. 셋업 변경으로 지령 간격이 어긋납니다. 거기서 비로소 창이 열려서, 두 번의 확인이 같은 틈에 떨어집니다.

테스트 중에는 나오지 않고 현장에서 나옵니다. 그리고 현장에서도 재현되지 않습니다. 이 성질은 테스트 공수가 부족해서 오는 것이 아닙니다. 여러 개의 축과 센서와 제어기가 동시에 움직이는 설계에는 특정한 인터리빙에서만 나타나는 상태가 있고, 테스트는 그 인터리빙을 고를 수단을 가지고 있지 않다 —— 는 구조에서 옵니다.

경쟁 상태, 교착 상태, 타이밍 의존 결함은 모두 이 한 무리입니다.

”해 봤지만 일어나지 않았다”와 “일어날 수 없다”

테스트 케이스를 쓰는 것은 사람입니다.

그래서 테스트가 확인하는 것은 설계자가 떠올린 케이스입니다. 커버리지 숫자는 쓴 케이스 중에서 얼마나 통과했는지를 재고 있습니다. 쓰지 않은 케이스는 분모에 들어 있지 않습니다. 상상력의 경계가 그대로 커버리지의 경계가 됩니다.

여기에 비대칭이 있습니다. 실패한 테스트는 정보가 많습니다. 무언가가 확실히 잘못돼 있습니다. 그러나 통과한 테스트가 알려 주는 것은 “이 한 건에서는 일어나지 않았다”는 것뿐입니다. 쓰지 않은 그 순서에 대해서는 아무 말도 하지 않습니다. 아무 말도 하지 않는데 초록색으로 보입니다.

모델 체킹은 이 부분을 기계적으로 합니다. 설계를 상태와 전이의 형태로 쓰고, 확인하고 싶은 성질을 씁니다. 그다음은 초기 상태에서 도달할 수 있는 상태를 하나부터 끝까지 조사합니다. “두 축이 공유 영역 안에 있는 상태는 도달 가능한가”에 대해, 도달 가능한 상태 전체를 조사해서 답합니다. 위의 스텝 1~5 같은 순서를 누군가가 떠올릴 필요는 없습니다. 떠올리지 못해도 도달 가능하다면 발견됩니다.

이것이 “해 봤지만 일어나지 않았다”와 “일어날 수 없다”의 차이입니다. 앞의 것은 시험해 본 범위에 대한 보고이고, 뒤의 것은 조사한 범위 전체에 대한 결론입니다.

실패했을 때 무엇이 돌아오는가

실무적인 차이가 하나 더 있습니다.

테스트가 실패했을 때 손에 들어오는 것은 assertion failed입니다. 어떤 조건이 깨졌는지는 알 수 있습니다. 왜 거기에 도달했는지는 직접 쫓아야 합니다.

검증이 깨졌을 때 돌아오는 것은 위반을 재현하는 이벤트 시퀀스입니다. 위의 스텝 1~5가 그대로 나옵니다. 이것을 반례라고 부릅니다. 읽어 보면 어느 틈을 통과했는지 알 수 있습니다. 자세한 내용은 반례란 무엇인가에 썼습니다.

솔직히 적어 두는 한계

좋은 이야기로 들렸다면 한계도 같은 밀도로 적어 둘 필요가 있습니다. 세 가지입니다.

하나. 설계밖에 확인하지 않습니다. 검증이 “일어날 수 없다”고 말하는 것은 설계에 대해서입니다. 그 설계대로 구현되어 있는지, 배선이 맞는지, 실물 장비의 모터가 상정한 시간에 멈추는지에 대해서는 아무 말도 하지 않습니다. 테스트는 줄지 않습니다. 줄어드는 것은 테스트로 찾아낼 생각이었는데 찾아내지 못했던 한 무리뿐입니다.

둘. 상태 폭발은 정말로 있습니다. 모든 상태를 조사하려면 상태 공간이 조사할 수 있는 크기 안에 들어와 있어야 합니다. 축을 늘리고, 상태 변수를 늘리고, 시간의 입도를 잘게 하면 조합은 지수적으로 늘어납니다. 그래서 모델은 추상화입니다. 무엇을 버릴지 고르는 것이 기량이고, 한계입니다. 너무 많이 버리면 실물 장비에 존재하지 않는 반례가 나옵니다. 너무 적게 버리면 검증이 끝나지 않습니다. 여기에 마법은 없습니다.

셋. 증명은 물어본 질문의 몫만큼만 답합니다. “두 축이 동시에 공유 영역에 들어가지 않는다”를 확인했다면 확인된 것은 그것뿐입니다. 세 번째 축 이야기도, 비상 정지에서의 복귀 이야기도 포함되어 있지 않습니다. 안전 성질을 올바르게 쓰는 것은 사람의 일입니다. 잘못된 질문을 세우면 잘못된 질문에 대한 자신 있는 답이 돌아옵니다. “전부 증명했습니다”라고 말하는 사람이 있으면 무엇을 증명했는지 물어보십시오.

그 위에서, 남는 것은 남습니다. 설계가 특정한 순서를 허용하고 있는지 아닌지는 실물 장비가 없어도, 아무도 떠올리지 못해도 기계적으로 확정할 수 있습니다. 그것뿐입니다. 그리고 그것만이 테스트로는 할 수 없는 일입니다.

다음에 읽을 글

검증이 깨졌을 때 돌아오는 이벤트 시퀀스를 현장에서 어떻게 읽고 어떻게 쓰는지는 반례란 무엇인가에서 다룹니다.

이 방법이 왜 취미의 이야기가 아니라 규격의 요구에 들어가 있는지는 왜 안전 규격은 형식기법을 요구하는가에 있습니다.