서 문

 프로세스 대수(PA: Process Algebra)를 처음 접한 것은 학부과정에서 운영체제 수업을 수강할 때였다. 당시 접한 PA는 최초의 공식적인 PA라고 할 수 있는 Hoare의 CSP[HOA85] 였는데, Unix의 fork-join 메카니즘에 기반을 둔 하위 단위의 병렬 프로그램들 또는 프로세스들과 비교할 수 있는 대표적인 상위 단위의 프로그래밍 언어로 이해되었다. 당시 코딩을 통해서 경험했던 CSP는 매우 간결하고 함축성이 높은 언어였으며, 이를 다른 언어와 비교하면 시(詩)와 소설(小說)의 차이라고나 할까? CSP 코드 자체는 이 상(李 箱)의 오감도(烏瞰圖)에 나오는 한 편의 시와 같은 느낌을 풍겼다. 여기에서 CSP로 작성된 factorial 함수 코드를 감상해 보자.

[    fact(i:1..maxproc)::       *[n: INTEGER;           fact(i-1)?n ->              [                n = 0 -> fact(i-1)!1             □                n > 0 -> fact(i+1)!n-1;                temp: INTEGER;                fact(i+1)?temp;                fact(i-1)!n*temp              ]        ] |    fact(0)::USER ]

특정 연산(computing) 공간에 최대 maxproc 만큼의 fact(i) 프로세스들이 존재한다. 각 fact(i) 프로세스들은 fact(i-1) 프로세스들로부터 ‘?’ 이라는 수신 통신 연산자를 통해 n 정수 값을 받는다. 이 값이 0이면, 그 fact(i-1) 프로세스에게 ‘!’이라는 발신 통신 연산자를 통해 1 정수 값을 돌려준다. 반대로 이 값이 0보다 크면, fact(i+1) 프로세스에게 ‘!’ 이라는 발신 통신 연산자를 통해 n-1 정수 값을 전해준다. 그리고 그 fact(i+1) 프로세스가 (n-1)! 값을 돌려주면, 이에 n을 곱하여 n! 값을 fact(i-1) 프로세스에게 ‘!’ 이라는 발신 통신 연산자를 통해 최종적으로 되돌려준다. 초기 fact(0)은 사용자이며, fact(1)에게 ‘!’이라는 발신 통신 연산자를 통해 정수 n 값을 입력하면, fact(0)은 fact(1)로부터 ‘?’ 이라는 수신 통신 연산자를 통해 n!의 값을 받게 된다.

예를 들면, 위에서 설명한 바와 같이 3!을 연산하는 과정을 도형적으로 기술하면 다음 그림과 같다. 즉, fact(0)이 fact(1)에게 3을 보내면, fact(1)은 3을 받아서, 3이 0이 아니면, fact(2)에게 3-1인 2를 보내고, fact(2)는 2을 받아서, 2가 0이 아니면, fact(3)에게 2-1인 1를 보내고, fact(2)는 1을 받아서, 1이 0이 아니면, fact(3)에게 1-1인 0를 보내고, fact(4)는 0을 받아서, 이 0이 0이면, fact(3)에게 1를 되돌려주고, fact(3)은 받은 이 1에 자신이 fact(2)에게서 받은 1을 곱해서 fact(2)에게 이 1*1을 되돌려주고, fact(2)는 받은 이 1*1에 자신이 fact(1)에게서 받은 2를 곱해서 fact(1)에게 이 2*1*1을 되돌려주고, fact(1)은 받은 이 2*1*1에 자신이 fact(0)에게서 받은 3을 곱해서 fact(0)에게 이 3*2*1*1을 되돌려준다. 즉, 3! 값을 되돌려준다.

과연 어떤 언어가, 특정 공간에 다수의 동일 유형 프로세스들이 병렬적으로 하나의 연산 목표를 위해서 동일 패턴의 연산과 상호작용(interaction)을 유기적으로 실행하는 과정을 CSP처럼 간결하고 함축적으로 표현할 수 있을까? 당시 이러한 CSP에 대한 경험은 필자에게 매우 충격적인 경험이었다. 그런데 우연인지 필연인지는 모르겠지만, 하나의 경험은 또 다른 경험으로 자연스럽게 연결이 되었다.

이후 필자는 대학원에서 ACSR[LDG91]을 접할 기회가 있었다. 이 ACSR은 실시간시스템(RTS: Real-Time Systems)의 명세를 위하여 Milner의 CCS[MIL89]에 시간과 자원경쟁 및 예외처리라는 개념을 추가적으로 도입한 PA였다. 그리고 ACSR로 명세된 RTS는 도달성 및 동일성에 대한 성질 및 특성들을 VERSA라는 도구를 통해 검증할 수 있었다.

당시 ACSR을 이해하기 위해서는 CCS를 이해해야 했었다. 하지만 CCS를 이해하는 것은 결코 쉬운 일이 아니었다. 특히 컴퓨터과학을 응용과학의 관점에서 운영하던 미국의 보편적인 교육 현실에서 볼 때 CCS의 기반이 되는 현대 수학의 대수 구조체에 대한 이해는 매우 난해해 보였다. 특히 동일성에 대한 다양한 해석과 의미는 이를 더욱 어렵게 만들었다. 외형적으로 같아 보이나, 내부적으로는 다른, 또는 내부적으로 같지 않으나 외형적으로 같은 등의 두 시스템 간의 다양한 동일성을 결정하는 τ-action과 이 액션의 복합적인 관계적 규칙들이, CCS를 실용적인 관점에서 이해하는 데 어려움을 초래했을 뿐만 아니라, 과연 CCS가 CSP처럼 실용적인지 의문을 갖게 만들었다. 하지만 기본적으로 이러한 CCS의 다양한 동일성들을 이해하고 나면, ACSR의 시간과 자원경쟁 및 예외처리의 속성들을 RTS 관점에서 이해하는 것은 어려운 일은 아니었다. 하지만, 그 배경이 되는 CCS의 동일성들과 비교해 보았을 때, 시간과 자원이라는 추가적인 차원과 Scope이라는 예외처리는 ACSR의 복잡도를 또 다른 차원과 경우에 대해 기하급수적으로 증폭시키는 문제를 초래한다고 판단이 되었다. 그러나 ACSR에서는 이러한 차원의 증폭 문제를 추가적인 동일성의 관점에서는 재해석하지 않은 부분이 있었을 뿐만 아니라, 예외처리가 가져오는 동일성의 위배에 대한 의미와 영향도 거론되지 않았다.

또 다른 관점에서 CCS 기반 ACSR을 CSP와 단순히 비교를 해보면, 다음과 같은 대표적인 차이가 있다고 판단되었다: CCS는 대수의 문법적 규범이 너무 강하고, ACSR은 예외처리의 범위가 너무 제한적이며, Nesting을 허용할 수 없을 정도로 규격화되어있다는 점이었다. 하지만, ACSR은 명세 언어로서 CSP의 간결성과 함축성에 CCS의 대수적 미학를 더하고, 시간의 공간에서 자원을 점유하기 위하여 서로 경쟁하는 오토마타들을 작동시키는 주술사의 주문과도 같았다. 즉, 위 CSP의 factoiral 예제를 통해 비교해 보면, 최대 maxproc 만큼의 fact(i) 프로세스들이 존재하는 특정 연산 공간에서, 각 fact(i) 프로세스들이 자신의 fact(i-1) 프로세스들과 fact(i+1) 프로세스들과의 통신을 통해서 n!의 연산을 유기적으로 수행할 때, 수행의 조건이 i 값이 0이거나 또는 n 값을 만족하는지에 대한 조건들에만 그치지 않고, 이 조건들이 ‘시간’이라는 차원에서 성립이 되는지를 판단해야 한다는 것과 비교할 수 있었다.

당시 필자가 접한, 그리고 경험한 ACSR은 매우 제한적이었다. 당시 박사논문 주제는 직장에서 개발 중이었던 SRE(SW Re/reverse-engineering Environment)[ML95] 도구에 재공학과 역공학 기능들을 추가하고 이들을 이론화하는 것이었다. 예를 들면, 추상성을 위한 RTS SW 아키텍처 정의 및 추출 도구 개발, 이를 기반으로 한 추상성 추출 및 관리, 기존 RTS SW에서의 OS 종속성을 해결하기 PL(Progamming Language) 및 SW 단계에서의 추상화 메커니즘의 개발과 번역 및 구축, 그리고 이 과정에서 생성되는 다양한 산물들(artifacts)의 시각화 등이었다. 특히 하위 단위 OS 단계에서의 프로세스들의 병렬성과 이들 간의 통신 및 제어 등과 같은 상호작용들을 상위 단위인 SW/PL 단계에서의 추상화된 프로세스들로 역공학하는 것은 매우 중요한 기능이었다. 당시 ACSR에 관심을 가지고 접근했던 이유도 바로 RTS SW 역공학 과정에서 기존 RTS SW에서 정의된 하위 단위 OS 단계의 프로세스들의 병렬성과 이들 간의 통신 및 제어 등과 같은 상호작용들을 ACSR 단계의 프로세스들과 이들 간의 상호작용으로 표현할 수 있는 가능성을 판단하기 위한 것이었다. 하지만, ACSR 같은 프로세스 대수들은 하위 단위 OS 단계의 프로세스들의 병렬성과 이들 간의 통신 및 제어 등과 같은 상호작용을 보장해주는 메커니즘이 구축되어 있지 않았고, 대수의 특성상 메커니즘의 필요성도 요구되지 않았다. 결국 이 역공학 과정에서 ACSR은 추상화의 대상으로서 적합하지 않다는 결론을 내리게 되었다. 이것이 필자가 대학원에서 접했던 ACSR에 대한 경험이었다.

이후 필자는 대학교에서 이전의 연구를 기반으로 하여, SW 역공학과 재공학을 순공학과 통합하여 하나의 순환공학으로 구축하는 연구에 매진하게 되었고, 이 연구의 대상은 이전 연구의 대상을 확장한 분산이동실시간시스템(DMRTS: Distributed Mobile Real-Time Systems)이었다. 특히 순공학의 설계과정에서 이동 객체들이 지정학적으로 분산된 환경에서 시간의 제약조건을 가지고 이동하는 성질을 명세하기 위한 방법으로써 정형기법을, 그리고 그 중 PA를 연구하게 되었다.

일반적으로 순공학의 설계과정에서 시스템과 SW를 명세하기 위한 정형기법에는 논리 기반, 상태도 기반, 그리고 PA 기반, 이렇게 세 개의 방법이 있다[CD96]. 이 중 DMRTS의 객체 또는 에이전트의 행동과 행위를 명세하기 위한 방법은 PA가 가장 적합해 보였다. 하지만, 특정 지정학적 공간에서 시간의 제약조건을 가지고 이동하며 상호작용하는 객체 또는 에이전트를 명세하는 데는 필자가 접한 CSP나 CCS는 적합하지 않았다. 왜냐하면, CSP와 CCS에는 프로세스의 이동성을 표현할 수 있는 기능성이 없기 때문이었다.

이 과정에서 접한 PA들이 π-calculus[MIL99], mobile ambients[CG98], bigraph[Mil01] 등이었다. 이러한 PA들은 지정학적-시간적 공간(Geo-Temporal Space) 내에서 에이전트들의 이동을 정형적으로 잘 표현할 수 있었다. 특히 에이전트들이 왜, 언제, 어디로 이동했는지를 수학적으로 명세, 분석, 검증할 수 있었다. 그리고 π-calculus의 경우 2006년 BPML(Business Process Modeling Language)[ARK02]와 마이크로소프트의 XLANG[THAT01]의 이론적 기반으로 사용되고 있을 만큼 그 활용범위는 매우 넓었다.

하지만 이러한 PA들은 에이전트들의 행위정보가 지정학적 공간과 시간적 공간 정보와 뒤섞여 활용함으로써 관계의 복잡도를 증가시키고 시스템에 이해도를 감소시키는 문제가 있다. 이를 정리하면 다음과 같다:

• π-calculus는 공간정보를 정의하지 않고 포트(port)를 가진 프로세스들의 동적인 연결 및 단절을 통해 이동 에이전트의 동적인 이동정보를 간접적으로 표현하고 있다.
• Mobile ambient(MA)는 프로세스가 속한 ambient의 범위를 통한 공간정보를 가지고 있고 ambient 간에 동적인 범위의 변화를 통해 프로세스의 이동정보를 표현하고 있다. 그러나 공간정보가 ambient의 이동정보에 종속이 되어 이동정보가 공간정보로 표현하지 못하는 상황이 발생될 수 있다.
• Bigraph는 이동 에이전트들의 행위 정보와 공간 정보를 그래프 형태로 표현하기 위한 메타 그래프이다. 최근에 π-calculus의 인터액션 기반의 모델링을 제시하고 있으나 bigraph에서는 공간정보에 행위정보들이 뒤섞여 있어 시스템 명세의 복잡성이 증가할 수 있다. 즉, 이들 모두 공간과 시간, 행위정보들이 하나의 명세에 뒤섞여서 동작 시 복잡성과 분석의 어려움들이 증가될 수 있다.

이러한 문제가 발생된 근본 원인은 대상 시스템들이 일반적으로 동적으로 변화되는 2 또는 3차원 공간정보와 그 공간에서 시간의 제약조건을 가진 이동 에이전트의 이동 및 통신 정보를 구분하여 표현할 수 있어야 함에도 불구하고 기존의 PA들이 이를 같은 공간 내에 모두 같이 명세했기 때문이라고 판단이 되었다.

즉 이러한 문제를 극복하기 위하여 새로운 개념의 PA가 요구되었고, 다음과 같은 PA들, 즉 CARDMI[JJ08]와 Onion[JS12]을 고안하게 되었다:

• CARDMI: DMRTS 명세 PA에 존재하는 공간, 행위, 시간에 의한 이해와 분석의 어려움을 극복하기 위하여, 시스템의 행위정보와 공간정보를 구분하여 명세 하기 위한 정형기법을 고안했다. 이 기법은 공간정보와 에이전트들의 행위정보(이동, 통신 등)를 구분하고, 행위는 이동과 인터액션으로 구분한다. 그리고 DMRS 에이전트의 순차성, 병렬성, 분산성, 이동성 등에 대한 모델링, 추상화, 동일성 검증 등을 제공한다.
• Onion: DMRTS을 시각화 하기 위한 PA 기반 도표 언어로 시스템을 ITL과 ITS의 융합된 관점을 제공하고, 요구사항 명세, 분석 그리고 검증에 대하여 전체적이며 일관된 시각화 방법을 제공한다. Onion은 프로세스 대수와 상태머신의 통합된 관점으로 표현하도록 디자인 되었다.

하지만 이러한 CARDMI와 Onion은 열약한 개발환경 때문에 온전한 도구로 제공되지 못했고, 이를 기반으로 한 관련 연구도 이 후 진행할 수 없었다. 이는 아마도 이론보다는 구현에 집중할 수 없는, 또는 이론적인 한계를 실용적인 도구로 구현할 수 없는 환경의 결과라는 생각이 든다.

이런 상황에서 2013년 오스트리아 비엔나 대학교의 OMiLAB이 제공하는 ADOxx Meta-Modeling Platform[FK13]을 사용할 수 있게 되었고, 이를 기반으로 CARDMI와 Onion의 가장 기본적인 특성에 다양한 유형의 이동성과 제어를 강화한 새로운 δ-Calculus[YM15]라는 PA를 고안하여 구현할 수 있게 되었다. 즉 ADOxx 상에서 δ-Calculus의 시각화를 기반으로, DMRTS를 명세 및 모의실험 하여, 이를 분석 및 검증할 수 있는 SAVE(Specification, Analysis, Verification and Evaluation) 프로토타입 도구를 개발하게 되었다[YM15, YGU15]. 이를 정리하면 다음과 같다:

• δ-Calculus: CARDMI와 Onion의 가장 기본적인 특성을 통합하고, 여기에 다양한 유형의 이동성, 즉 능동적 이동과 수동적 이동을 정의하고, 프로세스 생성 및 소멸, 휴지 및 생동 등과 같은 제어를 추가적으로 정의하였다. 기본적으로 모든 행동은 동기적이며, 비동기 또한 동기를 적용해 표현할 수 있도록 하였다.
• SAVE: SAVE는 δ-Calculus를 구현한 도구이다. DMRTS를 δ-Calculus로 명세하고, 이를 모의실험하여, 그 결과에 대하여 다양한 성질을 분석하고 검증할 수 있는 프로토타입 도구이다. 이는 ADOxx 메타-모델링 플랫폼에서 구현되었다.

본 연구서는 이렇게 필자가 접하고 연구한 PA들을 정리한 것이다. 여기에 나오는 자료들은 국제 논문지 및 학술지에 발표된 논문들을 한글로 번역하고 이를 연구서의 양식에 부합하도록 조정하였다. 그 정확성과 적합성을 위하여 각 유형 별 PA가 소개된 장(Chapter)별로 자료의 출처를 밝힌다. 이 연구서의 구성은 다음과 같다:

• 제1장: 이 장에서는 소프트웨어 개발 방법/활동과 이 과정에서 요구되는 정형기법과 이 정형기법 중 PA의 전반적인 내용을 간단하게 소개한다.
• 제2장: 이 장에서는 PA를 정의하고 이의 역사와 체계와 종류를 분류한다.
• 제3장: 이 장에서는 CCS를 소개한다.
• 제4장: 이 장에서는 CSP를 소개한다.
• 제5장: 이 장에서는 CCS에 시간의 속성을 추가한 TCCS를 소개한다.
• 제6장: 이 장에서는 CCS에 확률의 속성을 추가한 PCCS를 소개한다.
• 제7장: 이 장에서는 ACSR을 소개한다.
• 제8장: 이 장에서는 π-Calculus를 소개한다.
• 제9장: 이 장에서는 Mobile Ambient를 소개한다.
• 제10장: 이 장에서는 CARDMI를 소개한다.
• 제11장: 이 장에서는 CARDMI에 시간의 속성을 추가한 t-CARDMI를 소개한다.
• 제12장: 이 장에서는 Onion을 소개한다.
• 제13장: 이 장에서는 δ-Calculus를 소개한다.
• 제14장: 이 장에서는 연구서에 대한 결어 및 향후 연구를 제시한다.

그리고 부록에는 NEMO2014[NEMO]에서 발표했던 자료들을 정리하여 추가하였다. 이 자료는 DMRTS의 대표적인 예제인 EMS(Emergency Medical Systems)를 본 연구서에 소개된 PA들 중 다음 PA들로 명세하고, 이들이 실제 각 PA의 semantics에 의해 어떻게 실행이 되는지를 보이고, 이를 통해 각 PA의 특성들을 비교 및 분석할 수 있도록 하였다:

• A.1 CCS
• A.2 π-Calculus
• A.3 Mobile Ambient
• A.4 ACSR
• A.5 δ-Calculus

또한, 여기에 소개된 CARDMI, Onion 및 δ-Calculus는 필자가 지도했던, 그리고 지도하고 있는 대학원학생들과 같이 연구한 결과임을 밝힌다.

먼저 CARDMI는 저자의 지도를 받은 최정란 박사의 대표적인 연구결과이다. 이 CARDMI에서는 PA의 다양한 관점과 단계에서의 추상화와 동일성에 대한 연구가 이루어졌고, 학계에 발표가 되었다. 이 연구서에 소개된 내용은 이 중, 최정란 박사와 저자가 같이 연구하고 발표한 연구를 정리한 내용이다.

동일한 관점에서, Onion은 저자의 지도를 받은 온진호박사의 대표적인 연구결과이다. 이 Onion에서는 PA의 다양한 관점과 단계에서의 시각화와 동일성에 대한 연구가 이루어졌고, 학계에 발표가 되었다. 이 연구서에 소개된 내용은 이 중, 온진호 박사와 저자가 같이 연구하고 발표한 연구를 정리한 내용이다.

개인적으로 대학에서의 연구는 도전적이어야 한다고 생각한다. 왜냐하면, 대학은 실패의 결과를 수용할 수 있는 실험 정신에 기반을 두고 있기 때문이다. 산업체에서의 실패는 그 산업체의 존망을 결정하는 근거가 될 수 있지만, 대학에서의 실패는 더 큰 성공을 낳는 거름이 될 수 있다.

최정란 박사의 추상화에 대한 연구와 온진호 박사의 시각화에 대한 연구는 학문적으로 매우 도전적인 연구였다. 이론도 불완전했고, 개발환경도 척박했고, 저자의 지도 역량도 상대적으로 부족했다. 하지만, 저자는 누구도, 현실 - 이론, 개발, 논문, 과제 - 때문에, 시도하지 못했고, 시도할 수도 없었던, 그런 연구를 시도했다고 감히 말하고 싶다. 그리고 제자들이 이런 시도에 동참한 것에 고맙다는 말을 전하고 싶다.

그런 결과인지는 모르겠지만, 지금은 이런 연구의 결과를 최소한의 범위에서 입증할 수 있는 새로운 PA를 고안하게 되었다. 그 PA가 현재 박사과정 학생인 최영복군과 진행하고 있는 δ-Calculus이다. 이번 연구가 지난 연구와 다른 점은, 우연인지 필연인지는 모르겠지만, δ-Calculus를 구현할 수 있는 최소한의 안정된 개발환경, 즉 ADOxx Meta-Modeling Platform이 제공된다는 점이다. 이러한 환경에서 새로운 이론을 구현하기 위하여 SAVE 도구를 열심히 개발하고 있는 최영복군에게 감사의 말을 전하고 싶다. 그리고 여기에 소개한 일부 PA들은 실험실에서 최영복군과 같이 연구한 연구물들을 정리한 것이라는 것을 밝히고 싶다.

마지막으로, 이 연구서의 정리하면서, 필자는 최근 기법(method)이라는 용어에 대한 개념을 새롭게 인식할 수 있는 계기가 있었다. 이는 비엔나대학교의 Karagiannis 교수의 연구를 통해서였다.

필자는 개인적으로, 우리 실험실을 위해서, 또한 우리 대학과 우리 학계를 위해서, 2013년 7월, 일본 교토에서 개최된 37회 COMPSAC 학술대회에서 Karagiannis 교수를 만난 것을 행운이라고 생각한다. 같은 세션에서 그가 발표한 ADOxx Meta-Modeling 도구는 필자가 대학원과 직장에서 사용하던 meta-CASE 도구인 DECDesign을 연상하게 만들었다. 그에게 그 도구를 배울 수 있는 기회를 요청했고, 그가 제공한 교육과 환경은 최영복군이 연구하고 있는 δ-Calculus를 구현하기에 매우 적합한 도구가 되었다. 우리는 지금까지 2년 째, 이를 기반으로 δ-Calculus를 위한 SAVE라는 도구를 개발하고 있고, 매우 성공적인 결과를 만들어 내고 있다. 본 저서에 소개할 δ-Calculus도 2015년 유럽의 ECIS[YM15]와 eChallenge[YGM15]에 발표한 논문을 정리한 것이다. 이 자리를 빌어 Karagiannis 교수에게 감사의 말을 전하고 싶다.

그리고 첫 번째 연구서에 이렇게 두번째 연구서가 나오기까지 물심양면으로 후원해준 배진영 박사에 감사의 말을 전하고 싶다. 그리고 우리의 아이들, 령(昤)이와 안(顔)이에 고마움을 전한다. 이들은 나와 배진영 박사의 벅찬 행복이자 희망이다.

2015년 12월 28일

건지산 연구실에서