서 문

  

프로세스 대수(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) 프로세스들로부터 ‘?’ 이라는 수신 통신 연산자를 통해 정수 값을 받는다이 값이 0이면그 fact(i-1) 프로세스에게 ‘!’이라는 발신 통신 연산자를 통해정수 값을 돌려준다반대로 이 값이 0보다 크면, fact(i+1) 프로세스에게 ‘!’ 이라는 발신 통신 연산자를 통해 n-1 정수 값을 전해준다그리고 그 fact(i+1) 프로세스가 (n-1)! 값을 돌려주면이에 n을 곱하여 n! 값을 fact(i-1) 프로세스에게 ‘!’ 이라는 발신 통신 연산자를 통해 최종적으로 되돌려준다초기 fact(0)은 사용자이며, fact(1)에게 ‘!’이라는 발신 통신 연산자를 통해 정수 값을 입력하면, 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! 값을 되돌려준다.


csp-factorial-new.png

 

과연 어떤 언어가특정 공간에 다수의 동일 유형 프로세스들이 병렬적으로 하나의 연산 목표를 위해서 동일 패턴의 연산과 상호작용(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!의 연산을 유기적으로 수행할 때수행의 조건이 값이 0이거나 또는 값을 만족하는지에 대한 조건들에만 그치지 않고,이 조건들이 시간이라는 차원에서 성립이 되는지를 판단해야 한다는 것과 비교할 수 있었다.

 

당시 필자가 접한그리고 경험한 ACSR은 매우 제한적이었다당시 박사논문 주제는 직장에서 개발 중이었던 SRE(SW Re/reverse-engineering Environment)[ML95] 도구에 재공학과 역공학 기능들을 추가하고 이들을 이론화하는 것이었다예를 들면추상성을 위한RTS SW 아키텍처 정의 및 추출 도구 개발이를 기반으로 한 추상성 추출 및 관리기존 RTS SW에서의 OS 종속성을 해결하기 위한 PL(Programming 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가 가장 적합해 보였다하지만,특정 지정학적 공간에서 시간의 제약조건을 가지고 이동하며 상호작용하는 객체 또는 에이전트를 명세하는 데는 필자가 접한 CSPCCS는 적합하지 않았다왜냐하면, 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에서는 공간정보에 행위정보들이 뒤섞여 있어 시스템 명세의 복잡성이 증가할 수 있다이들 모두 공간과 시간행위정보들이 하나의 명세에 뒤섞여서 동작 시 복잡성과 분석의 어려움들이 증가될 수 있다.


이러한 문제가 발생된 근본 원인은 대상 시스템들이 일반적으로 동적으로 변화되는 또는 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

건지산 연구실에서