당신이 모든 연주자가 로봇이자 신호등이며 동시에 스마트폰인, 거대하고 혼란스러운 오케스트라를 지휘하려고 한다고 상상해 보십시오. 그들은 모두 서로에게 동시에 말을 걸고, 메모와 지시사항, 그리고 데이터를 주고받으려 합니다. 만약 한 연주자가 틀린 음을 연주하거나, 두 로봇이 정확히 같은 밀리초(millisecond)에 동일한 문손잡이를 잡으려고 한다면, 전체 시스템은 충돌하거나, 멈추거나, 위험한 행동을 할 수 있습니다. 이것이 바로 '상호작로하는 시스템(interacting systems)'의 세계입니다. 즉, 우리의 자동차, 전력망, 인터넷을 실행하는 소프트웨어의 복잡한 네트워크입니다. 문제는 이러한 시스템이 너무나 복잡해서 인간의 뇌로는 오류가 발생할 수 있는 숨겨진 함정을 찾아내기 어렵다는 점입니다. 이를 해결하기 위해 과학자들은 이 시스템이 어떻게 작동하는지를 정확하게 설명하는 특별한 종류의 '수학적 언어'를 사용하며, 이를 통해 엉킨 코드들을 하나의 깨끗하고 논리적인 이야기로 바꾸어 실제 소프트웨어가 구축되기 전에 오류를 확인할 수 있게 합니다.

이 논문은 이 혼란스러운 시스템들을 위한 궁극적인 번역기가 되기 위해 만들어진 $\mu$CRL과 mCRL2라는 두 가지 언어의 이야기를 들려줍니다. 이들은 세 가지 강력한 아이디어를 결কে합한 보편적인 규칙서와 같습니다: 프로세스 대수(Process Algebra) (메시지 보내기나 문 열기와 같은 동작을 기술하는 방식), 추상 데이터 타입(Abstract Data Types) (숫자나 리스트와 같이 전달되는 데이터를 완벽한 정밀도로 정의하는 방식), 그리고 양상 논리(Modal Logic) ("시스템이 항상 멈출 것인가?" 또는 "막힐 가능성이 있는가?"와 같은 질문을 던지는 방식)입니다. 저자인 Jan Friso Groote와 Erik P. de Vink는 이 도구들이 1980년대의 단순한 아이디어에서 어떻게 오늘날 페이스메이커(심박 조율기)부터 철도 시스템에 이르기까지 검증에 사용되는 정교한 툴킷으로 진화했는지 설명합니다. 그들은 이 도구들이 단순히 손으로 증명을 적는 방식에서 어떻게 수백만 가지의 시나리오를 자동으로 점검하여 디지털 세상이 무너지지 않도록 보장하는 거대한 엔진으로 성장했는지 보여줍니다.

언어의 이야기: 거대한 혼돈에서 매끄러운 도구로

이야기는 1980년대 암스테르담의 수학자 그룹이 큰 문제에 직면하면서 시작되었습니다. 그것은 바로 복잡한 컴퓨터 시스템을 세부 사항에 매몰되지 않고 어떻게 설명할 것인가 하는 문제였습니다. 그들은 컴퓨터 시스템을 일련의 동작으로 취급하는 프로세스 대수라는 개념에서 시작했습니다. 로봇이 "걷기", "말하기", 또는 "기다리기"를 할 수 있다고 상상해 보십시오. 이러한 동작들은 차례대로 일어날 수도 있고, 동시에 일어날 수도 있습니다. 하지만 초기 버전의 언어들은 장난감 상자에 몇 개의 블록만 들어있는 것과 같았습니다. 로봇의 움직임은 설명할 수 있었지만, 로봇이 운반하는 데이터(예: 숫자 리스트나 복잡한 메시지)는 다룰 수 없었습니다.

이를 해결하기 위해 연구자들은 모든 다른 언어를 하나의 마스터 형식으로 번역할 수 있는 '공통 표현 언어(Common Representation Language, CRL)'를 구축하려고 노력했습니다. 이는 마치 세상의 모든 플러그에 맞는 거대한 유니버설 어댑터를 만들려는 것과 같았습니다. 그러나 그 어댑터는 너무 거대하고 복잡해져서 사용할 수 없는 지경에 이르렀습니다. 그것은 마치 모든 언어의 모든 단어와 모든 가능한 정의 및 유의어를 포함하는 사전을 만들려는 것과 같았으며, 결국 너무 무거워 들어 올릴 수 없게 되었습니다. 팀은 거대하고 포괄적인 언어 대신, 작고 날카로우며 우아한 것이 필요하다는 것을 깨달았습니다. 그래서 그들은 $\mu$CRL(pronounced "micro-CRL")을 만들었습니다.

$\mu$CRL은 "마이크로" 버전이었습니다. 즉, 동작(프로세스)을 기술하는 능력과 단순한 방정식을 사용하여 데이터(숫자나 리스트 등)를 정의하는 능력을 결합한 작고 압축된 언어였습니다. 이 언어는 수학적으로 아름답고 정밀하도록 설계되었습니다. 초기에 사람들은 시스템이 올바른지 증명하기 위해 $\mu$CRL을 사용하여 긴 수동 증명을 작성했습니다. 이는 마치 탐정이 용의자의 무죄를 입증하기 위해 50페이지짜리 보고서를 손으로 직접 쓰는 것과 같았습니다. 이 방식은 작은 사례에는 효과적이었지만, 현실 세계의 거대하고 복잡한 시스템을 다루기에는 너무 느렸습니다.

업그레이드: mCRL2의 등장

2000년경, 팀은 $\mu$CRL에 몇 가지 어색한 습관이 있다는 것을 깨달았습니다. 그것은 마치 잘 달리는 자동차인데 핸들이 돌리기 어렵고 대시보드가 혼란스러운 것과 같았습니다. 예를 들어, 시스템의 서로 다른 부분들이 어떻게 통신하는지 설명하는 방식이 투박했고, 데이터를 다루는 방식도 다소 경직되어 있었습니다. 그래서 그들은 언어를 업그레이드하기로 결정했고 이름을 mCRL2로 변경했습니다.

여기서 "2"는 단순히 '버전 2'를 의미하는 것이 아니라, 새로운 시작을 의미했습니다. 그들은 핵심 수학은 유지하되 언어를 훨씬 더 사용자 친화적이고 강력하게 만들었습니다.

• 더 나은 데이터: 이전 버전에서는 벽을 만들 때마다 집을 짓는 것처럼 모든 숫자와 리스트를 처음부터 정의해야 했습니다. mCRL2에서는 "표준 라이브러리"(표준 숫자, 리스트, 집합 등 미리 만들어진 벽돌)를 추가하여, 사용자가 제조가 아닌 설계에 집중할 수 있게 했습니다. 또한 "고차 함수(higher-order functions)"를 추가하여 함수를 데이터처럼 다룰 수 있게 함으로써 언어의 표현력을 높였습니다.
• 더 똑똑한 통신: 이전 언어에서 시스템의 두 부분이 서로 대화하도록 하는 것은, 모든 사람이 매우 엄격한 특정 단계에 동의해야 하는 군무를 조율하는 것과 같았습니다. mCRL2는 "멀티 액션(multi-actions)"을 도입하여, 여러 일이 자연스럽게 동시에 일어날 수 있도록 했습니다. 이는 마치 친구들이 동시에 하이파이브를 하는 것과 같습니다.
• 시간과 확률: 새로운 버전은 시간(예: "5초 기다리기")과 확률(예: "이 일이 일어날 확률이 10%이다")을 다룰 수 있는 기능을 추가하여, 완벽하고 예측 가능한 기계가 아닌 실제 세계의 시스템을 모델링할 수 있게 했습니다.

도구 세트: 손글씨에서 슈퍼컴퓨터로

이 이야기의 가장 흥ло로운 부분은 이 팀이 이 언어를 어떻게 거대한 툴킷으로 탈바꿈시켰는가 하는 점입니다. 처음에는 시스템이 올바른지 확인하려면 인간이 수학을 읽고 단계별로 증명해야 했습니다. 하지만 시스템이 커짐에 따라 이는 불가능해졌습니다. 팀은 이 힘든 작업을 수행할 수 있는 컴퓨터 프로그램 모음(툴 세트)을 구축했습니다.

수십억 개의 경로가 있는 도시의 지도를 가지고 있다고 상상해 보십시오. 인간은 막다른 길을 찾기 위해 모든 경로를 걸어 다닐 수 없습니다. 하지만 mCRL2 도구는 "상태 공간(state space)", 즉 시스템이 처할 수 있는 모든 상황의 거대한 지도를 생성할 수 있습니다.

• 리니어라이저(The Lineariser): 이 도구는 복잡하고 엉망인 시스템 설명을 단순하고 직선적인 규칙 목록으로 평탄화하여 분석하기 쉽게 만듭니다.
• 상태 공간 생성기(The State Space Generator): 이 도구는 지도를 만듭니다. 초당 수백만 개의 상태를 생성할 수 있습니다. 과거에는 컴퓨터가 수백만 개의 상태만을 처리할 수 있었지만, 오늘날 64비트 머신과 영리한 기술을 통해 이 도구들은 최대 $10^{10}$(100억) 개의 상태를 가진 시스템을 처리할 수 있습니다.
• 모델 체킹(Model Checking): 이것은 마법 지팡이입니다. 당신은 특수한 논리 언어로 질문을 던집니다(예: "로봇이 언젠가 갇히게 될까?"). 그러면 도구는 전체 지도를 확인하여 답이 "예"인지 "아니오"인지 알려줍니다. 만약 답이 "아니오"라면, 도구는 단순히 "고장 났다"라고 말하는 데 그치지 않고, 시스템이 어떻게 실패했는지를 보여주는 구체적인 사례(counter-example), 즉 운전자가 어디서 실수를 했는지 보여주는 자동차 사고 재현 영상과 같은 이야기를 제공합니다.

실제 세계의 성과와 향후 과제

이 논문은 이 도구들이 단순히 이론을 위한 것이 아니라, 실제 중요한 시스템을 검증하는 데 사용되었음을 보여줍니다. 저자들은 페이스메이커의 소프트웨어, 파이어와이어(firewire) 프로토콜, 심지어 네덜란드의 메슬란트(Maeslant) 방벽 제어 시스템을 검증하는 데 mCRL2를 사용했다고 언급합니다. 한 유명한 사례에서는 교과서에 기술된 통신 프로토콜에서 숨겨된 "라이브락(livelock)" 버그를 발견했습니다. 이 버그는 매우 특정한 희귀한 조건에서 시스템을 영원히 멈추게 만드는 버그였습니다. 교과서 저자는 데이터가 정확히 적절한 순간에 손실될 때만 발생하는 이 버그를 수년간 알지 못했습니다. mCRL2 도구는 이를 즉시 찾아냈습니다.

저자들은 자신들이 무엇을 달성했는지, 그리고 무엇이 여전히 진행 중인 작업인지 매우 명확하게 밝히고 있습니다. 그들은 수학적으로 건전하고 실질적으로 유용한 프레임워크를 성공적으로 구축했습니다. 그들은 형식적 방법론(formal methods)이 소프트웨어의 품질을 10배 높이고 효율성을 3배 높일 수 있음을 입증했습니다. 그러나 도구가 아직 완벽하지는 않다고 인정합니다.

• 상태 공간 문제: 최고의 도구를 사용하더라도, 어떤 시스템은 너무 거대해서 모든 가능성의 "지도"가 컴퓨터 메모리에 담기지 않을 수 있습니다. 그들은 이러한 지도를 압축하기 위한 "심볼릭(symbolic)" 방법을 연구하고 있지만, 여전히 도전 과제입니다.
• "이상적인" 스타일: 그들은 아직 이러한 모델을 작성하는 단 하나의 "완벽한" 방법이 없다는 점을 지적합니다. 이야기를 쓰는 방법이 다양하듯 모델을 만드는 방법도 다양하며, 어떤 방식은 분석을 훨씬 어렵게 만듭니다. 그들은 여전히 최선의 "스타일"을 찾아가는 과정에 있습니다.
• 연속 시간과 확률: 단순한 시간과 확률은 다룰 수 있지만, 연속적인 실제 세계의 확률(예: 심장 박동의 정확한 타이밍)을 다루는 수학은 여전히 연구 중입니다.

큰 그림

논문은 희망적이면서도 현실적인 전망으로 결론을 맺습니다. 저자들은 컴퓨터가 더 빨라지고 시스템이 더 복잡해짐에 따라(AI 및 사이버 물리 시스템과 함께), 이러한 수학적 도구에 대한 필요성이 더욱 커질 것이라고 믿습니다. 그들은 mCRL2가 미분 방정식이 다리나 엔진을 설계하는 표준 언어인 것처럼, 시스템 설계의 "링구아 프랑카(lingua franca, 공용어)"가 되는 미래를 꿈꿉니다.

그들은 자신들의 성공이 두 가지 규칙을 고수했기 때문이라고 강조합니다: 수학적 엄밀성(수학이 완벽한지 확인하는 것)과 실질적 관련성(실제로 더 나은 시스템을 만드는 데 도움이 되는지 확인하는 것)입니다. 그들은 단순히 예쁜 수학을 쓰고자 한 것이 아니라, 실제 세계의 시스템이 멈추는 것을 막고 싶었습니다. 아직 모든 문제를 해결하지는 못했지만, 그들은 엔지니어들이 코드 속의 보이지 않는 함정을 볼 수 있게 하여 우리가 의존하는 디지털 세상이 안전하고 신뢰할 수 있으며 의도한 대로 작동하도록 돕는 강력한 엔진을 구축했습니다.