현장에서 올라오는 보고 중에 가장 곤란한 것이 이겁니다.
“가끔 멈춥니다”
재현 절차는 없습니다. 로그는 있지만 멈춘 전후만 보일 뿐입니다. 장비는 눈앞에서 멀쩡히 돌아갑니다. 수십 번을 돌려도 멈추지 않습니다. 그런데도 보고는 올라와 있고, 대책은 써야 합니다.
이때 정말로 필요한 것은 원인의 이름이 아닙니다. 그 순서입니다. 무엇이 일어나고, 다음에 무엇이 일어나면 그 상태가 되는가. 그것만 알면 나머지는 대단한 일이 아닙니다.
우리에게 익숙한 에러는 경로를 알려주지 않습니다
현장에서 에러가 손에 들어오는 형태는 대체로 두 가지입니다.
하나는 현장 보고입니다. “가끔 멈춥니다”, “드물게 알람이 뜹니다”. 현상은 알 수 있지만 경로를 알 수 없습니다.
다른 하나는 테스트 실패입니다. “assertion failed”. 어떤 조건이 어느 줄에서 깨졌는지는 알 수 있습니다. 하지만 왜 거기에 도달했는지는 알 수 없습니다. 테스트가 준 입력에서 그 앞은 직접 따라가야 합니다.
둘 다 깨진 결과는 알려줍니다. 깨지기까지의 경로는 알려주지 않습니다.
설계를 검증한다는 것은 이 지점이 다릅니다. 설계에 “도어가 열려 있는 동안 가동부는 동작하지 않는다”라고 써 놓고, 그것이 정말로 성립하는지를 기계적으로 조사하게 합니다. 성립하지 않을 때 돌아오는 것은 “성립하지 않습니다”라는 한 줄이 아닙니다. 성립하지 않게 되는 이벤트 시퀀스가 순서대로 나열되어 돌아옵니다. 이것을 반례라고 부릅니다.
반례는 자동 생성된 재현 절차입니다.
반례 하나를 따라 걸어봅니다
교과서적인 장비를 하나 생각합니다. 반송 암과 Z축, 그리고 도어 인터록을 가진 흔한 구성입니다.
안전 조건은 하나입니다.
도어가 열려 있는 동안 가동부는 동작하지 않는다.
이것을 검증에 걸면 예를 들어 이런 시퀀스가 돌아옵니다.
1. 초기 상태: 도어=닫힘, Z축=상승단, 반송=대기, 인터록=해제
2. 작업자가 도어 열림 버튼을 누름 → 도어=개방 중(기계적으로 움직이기 시작)
3. 상위가 반송 시작을 지령 → 반송=동작 중
4. 도어 센서가 개방을 감지 → 도어=열림, 인터록 요구를 발행
5. 인터록이 정지를 요구 → 반송=감속 중
위반: 스텝 4 시점에 도어=열림 이면서 반송=동작 중
안전 조건 "도어가 열려 있는 동안 가동부는 동작하지 않는다"가 깨짐읽어야 할 곳은 스텝 2와 4 사이입니다.
도어 열림 버튼이 눌린 시점부터 도어 센서가 개방을 감지할 때까지 틈이 있습니다. 설계상으로는 “도어 열림 → 인터록 → 정지”가 한 줄로 보였습니다. 하지만 실제로는 버튼과 감지가 별개의 사건이고, 그 사이로 상위의 지령이 끼어들 수 있습니다. 반례는 그 틈을 통과하는 절차를 구체적으로 하나 제시합니다.
여기서부터는 늘 하던 설계 작업입니다. 버튼을 누른 시점에 인터록 요구를 낼 것인가. 상위의 반송 시작 지령에 도어 상태 조건을 붙일 것인가. 정지에 걸리는 시간까지 포함해서 안전 조건을 다시 쓸 것인가. 무엇을 고를지는 설계 판단이지만, 무엇을 논의해야 하는지는 이미 손에 들어와 있습니다.
”설계 문제인가, 구현 문제인가”가 사라집니다
장비 디버깅에서 비싼 것은 고치는 시간이 아닙니다. 어디가 잘못됐는지 밝혀내는 시간입니다. 그리고 그 첫걸음은 언제나 이겁니다 ——
“이건 설계 문제인가, 구현 문제인가”
반례는 이 질문을 건너뜁니다. 반례가 보여주는 것은 구현의 버그가 아닙니다. 설계가 그 절차를 허용하고 있다는 사실입니다. 코드를 한 줄도 보지 않은 단계에서, 실물 장비를 만지지 않은 채로 그것이 확정됩니다.
“어딘가 이상하다”와 “이 순서로 일어나면 이상하다”의 차이가 디버깅 몇 주 분입니다.
리뷰할 수 있다는 것
반례의 가장 실무적인 성질은 아마 이것입니다. 사람이 읽을 수 있습니다.
돌아오는 것은 증명의 내부도, 도구 고유의 기호도 아닙니다. 설계에서 쓰는 어휘 —— 신호, 상태, 전이 —— 가 나열된 시퀀스입니다. 그래서 설계 리뷰에 그대로 가져갈 수 있습니다. 화면에 띄워 놓고 위에서부터 짚어 내려가며 “여기서 반송이 움직이기 시작한다”, “여기서 감지가 들어온다”라고 설명할 수 있습니다.
이것은 “도구가 문제가 있다고 합니다, 믿어 주십시오”와는 전혀 다른 이야기입니다. 반례는 주장이 아니라 절차입니다. 절차라면 그 자리에 있는 전원이 함께 확인할 수 있습니다. 반례가 타당한지 판단하는 데 검증의 내부를 이해할 필요는 없습니다. 장비를 이해하고 있으면 충분합니다.
그리고 한번 손에 넣은 이벤트 시퀀스는 그대로 테스트 케이스가 됩니다. 실물 장비가 나오면 이 순서대로 조작해서 확인하면 됩니다. 수정한 뒤의 회귀 시나리오로도 남길 수 있습니다. 반례는 그때 한 번 쓰고 마는 지적이 아니라, 자산으로 남는 형태를 하고 있습니다.
반례가 설계가 아니라 모델을 가리킬 때
솔직하게 적어 둡니다.
반례를 읽고 “이 절차는 실물 장비에서는 일어나지 않는다”고 생각할 때가 있습니다. 자주 있습니다. 그리고 그 직관은 종종 맞습니다.
원인은 대개 두 가지입니다.
하나는 안전 조건을 쓴 방식이 틀렸던 경우입니다. “도어가 열려 있는 동안”의 “열림”을 버튼 누름으로 생각하고 썼는지, 센서 감지로 생각하고 썼는지. 애매한 채로 쓰면 의도하지 않은 해석의 시퀀스가 나옵니다.
다른 하나는 모델이 너무 느슨했던 경우입니다. 실물 장비에서는 기계적으로 동시에 일어날 수 없는 두 사건을, 모델에서는 서로 독립적으로 일어날 수 있게 만들어 버린 것입니다. 그러면 현실에는 존재하지 않는 절차가 반례로 나옵니다.
둘 다 실패가 아닙니다. 어느 쪽이든 자신이 설계를 정확하게 쓰지 못하고 있었다는 사실을 알게 된 것입니다. “열림이란 무엇인가”를 애매하게 놔둔 채 몇 년을 돌려온 설계서는 드물지 않습니다. 반례는 그 애매함을 구체적인 절차의 형태로 들이밉니다.
다만 이것도 솔직히 말해 둘 필요가 있습니다. 반례를 읽는 것도 익혀야 하는 기술입니다. 처음에는 설계의 오류와 모델의 오류를 구별하는 데 시간이 걸립니다. 몇 개 읽어 보면 익숙해집니다. 익숙해지기 전까지는, 익숙해지는 데 걸리는 시간이 듭니다.
유한한 시퀀스와 끝나지 않는 루프
보충을 하나 하겠습니다.
반례의 형태는 확인하려는 성질에 따라 두 종류가 있습니다.
“나쁜 일이 일어나지 않는다” 유형의 조건 —— 도어가 열려 있는 동안 가동부가 움직이지 않는다, 두 축이 동시에 간섭 영역에 들어가지 않는다 —— 이 깨질 때는 나쁜 상태에 이르는 유한한 이벤트 시퀀스가 돌아옵니다. 위의 예가 이것입니다.
“좋은 일이 언젠가 일어난다” 유형의 조건 —— 원점 복귀를 지령하면 반드시 원점에 도달한다, 비상 정지에서는 반드시 복귀할 수 있다 —— 이 깨질 때는 그 좋은 일이 일어나지 않은 채 계속 도는 루프가 돌아옵니다. 두 상태를 오가면서 언제까지나 원점에 도달하지 않습니다. 장비로 말하면 행(hang)입니다.
어느 쪽이든 읽는 법은 같습니다. 위에서부터 순서대로 사건을 따라갑니다.
다음에 읽을 글
반례가 돌아오는 것은 테스트와는 다른 방식으로 조사하기 때문입니다. 테스트는 골라낸 절차를 시험하고, 설계 검증은 절차 전체를 조사합니다. 그 차이는 테스트와 형식기법은 무엇이 다른가에서 다룹니다.
애초에 왜 장비 소프트웨어는 실물 장비에 의존할 수밖에 없었는가. 그 구조는 왜 장비 소프트웨어는 V자 모델의 오른쪽 절반을 실행할 수 없는가에 있습니다.