분산 공정의 구축 및 분석
Construction and Analysis of Distributed Processes | |
| 개발자 | 인리아 볼록스팀(이전 바시팀) |
|---|---|
| 초기 릴리즈 | 1989년 32~33년 전 |
| 안정적 해제 | 2020 / 2020년 12월 13일; 전 |
| 운영 체제 | Windows, MacOS, Linux, Solaris 및 OpenIndiana |
| 유형 | 통신 프로토콜 및 분산 시스템 설계를 위한 도구 상자 |
| 웹사이트 | 캐드핀리아 |
CADP[1](Construction and Analysis of Distributed Process)는 통신 프로토콜 및 분산 시스템 설계를 위한 툴박스다.CADP는 INRIA Rone-Alpes에서 COLOBCS 팀(이전의 VASIS 팀)에 의해 개발되며 다양한 보완 툴과 연결된다.CADP는 유지되고 정기적으로 개선되며 많은 산업 프로젝트에서 사용된다.
CADP 툴킷의 목적은 시뮬레이션, 신속한 애플리케이션 개발, 검증 및 테스트 생성을 위한 소프트웨어 도구와 함께 공식적인 설명 기법을 사용하여 신뢰할 수 있는 시스템의 설계를 촉진하는 것이다.
CADP는 비동기 동시성으로 구성되는 시스템, 즉 인터리빙 의미론에 의해 관리되는 병렬 프로세스 세트로 동작이 모델링될 수 있는 시스템에 적용될 수 있다.따라서 CADP는 하드웨어 아키텍처, 분산 알고리즘, 통신 프로토콜 등을 설계하는 데 사용될 수 있다.CADP에서 구현된 열거적 검증(명시적 상태 검증이라고도 함) 기법은 그러한 정리를 입증하는 것은 아니지만 복잡한 시스템에서 설계 오류를 자동으로 비용 효율적으로 탐지할 수 있다.
CADP에는 신뢰할 수 있는 시스템 설계에 필요한 두 가지 접근방식의 공식적 방법 사용을 지원하는 도구가 포함되어 있다.
- 모델은 병렬 프로그램 및 관련 검증 문제에 대한 수학적 표현을 제공한다.모델의 예로는 오토마타, 통신 오토마타 네트워크, 페트리 네트, 이항 결정도, 부울 방정식 시스템 등이 있다.이론적인 관점에서 모델에 대한 연구는 특정한 기술 언어와 무관하게 일반적인 결과를 추구한다.
- 실제로 모델은 복잡한 시스템을 직접 설명하기에는 너무 초보적인 경우가 많다(이는 지루하고 오류가 발생하기 쉽다).높은 수준의 설명을 검증 알고리즘에 적합한 모델로 변환하는 컴파일러뿐만 아니라 이 작업에는 프로세스 대수 또는 프로세스 미적분학으로 알려진 더 높은 수준의 형식주의가 필요하다.
역사
1986년 CADP에 대한 작업이 시작되었는데, 이때 처음 두 도구의 개발인 카이사르와 알데바란(Aldebaran)이 착수되었다.1989년에는 CADP 약어가 만들어졌는데, CADE/ALDEBARAN 유통 패키지를 의미했다.시간이 지남에 따라, 도구를 사용할 수 있는 프로그래밍 인터페이스를 포함하여 몇 가지 도구가 추가되었다. CADP 약어는 그 후 CASERS/ALDEBARAN 개발 패키지가 되었다.현재 CADP에는 50개 이상의 도구가 포함되어 있다.동일한 약어를 유지하면서도 툴박스의 명칭은 그 목적을 보다 잘 나타내도록 변경되었다.분산 프로세스의 구축 및 분석.
주요 릴리스
CADP의 발매는 알파벳 문자("A"에서 "Z"까지)로 연속적으로 명명된 다음, 학술연구그룹을 주최하는 도시의 이름이 LOTOS 언어에 적극적으로 작용하고, 보다 일반적으로 동시성 이론에 크게 공헌한 도시의 이름들로 이루어졌다.
| 코드명 | 날짜 |
|---|---|
| "A"… "Z" | 1990년 1월 - 1996년 12월 |
| 20대 | 1997년 6월 |
| 리게 | 1999년 1월 |
| 오타와 | 2001년 7월 |
| 에든버러 | 2006년 12월 |
| 취리히 | 2013년 12월 |
| 암스테르담 | 2014년 12월 |
| 스토니 브룩 | 2015년 12월 |
| 옥스퍼드 | 2016년 12월 |
| 소피아 안티폴리스 | 2017년 12월 |
| 웁살라 | 2018년 12월 |
| 피사 | 2019년 12월 |
| 알보리 | 2020년 12월 |
| 사르브뤼켄 | 2021년 12월 |
주요 릴리스 간에는 종종 마이너 릴리스가 제공되어 새로운 기능과 개선 사항에 대한 조기 액세스를 제공한다.자세한 내용은 CADP 웹 사이트의 변경 목록 페이지를 참조하십시오.
CADP 기능
CADP는 단계별 시뮬레이션에서 대규모 병렬 모델 확인에 이르기까지 다양한 기능을 제공한다.여기에는 다음이 포함된다.
- 몇 가지 입력 형식에 대한 컴파일러:
- BCG_MIN 및 BISIMULTER와 같은 몇 가지 동등성 검사 도구(최소화 및 비교 모듈화 관계)
- Evaluator 및 XTL과 같은 다양한 시간적 논리학 및 mu-mulus에 대한 여러 모델 체커.
- 열거형 검증, 즉석 검증, 바이너리 의사결정도를 이용한 심볼 검증, 구성 최소화, 부분 주문, 분산형 모델 확인 등 여러 검증 알고리즘이 결합됐다.
- 시각적 검사, 성능 평가 등과 같은 고급 기능을 갖춘 기타 도구
CADP는 모듈식으로 설계되어 있으며, CADP 도구를 다른 도구와 결합하고 다양한 사양 언어에 적응시킬 수 있는 중간 형식과 프로그래밍 인터페이스(BCG, OPEN/CASAR 소프트웨어 환경 등)를 강조한다.
모델 및 검증 기법
검증은 복잡한 시스템을 시스템의 의도된 기능을 특징짓는 속성 집합(예: 교착된 자유, 상호 배제, 공정성 등)과 비교하는 것이다.
CADP에서 대부분의 검증 알고리즘은 상태 집합, 초기 상태 및 상태 간의 전환 관계로 구성되는 라벨링된 전환 시스템(또는 단순하게 자동 또는 그래프) 모델에 기초한다.이 모델은 종종 연구 대상 시스템의 높은 수준의 설명에서 자동으로 생성되며, 다양한 의사결정 절차를 사용하여 시스템 속성과 비교된다.속성을 표현하는 데 사용되는 형식주의에 따라 다음 두 가지 접근법이 가능하다.
- 행동 속성은 시스템의 의도된 기능을 automata(또는 더 높은 수준의 설명, 즉 automata로 번역)의 형태로 표현한다.이러한 경우, 검증에 대한 자연스러운 접근방식은 동등성 검사로, 시스템 모델과 그 특성(둘 다 automata로 표시됨)을 비교하는 것으로 구성되며, 어느 정도의 동등성 또는 사전 주문 관계를 나타낸다.CADP는 다양한 동등성 및 사전 주문 관계를 비교 및 최소화하는 동등성 검사 도구를 포함하고 있다. 이러한 도구 중 일부는 확률적 모델과 확률론적 모델(예: 마르코프 체인)에도 적용된다.또한 CADP에는 시스템의 그래픽 표현을 확인하는 데 사용할 수 있는 육안 검사 도구가 포함되어 있다.
- 논리적 속성은 시스템의 의도된 기능을 시간적 논리 공식의 형태로 표현한다.그러한 경우 검증에 대한 자연스러운 접근방식은 모델 확인으로, 시스템 모델이 논리적인 특성을 만족하는지 여부를 결정하는 것으로 구성된다.CADP는 강력한 형태의 시간 논리인 모달 무 미적분학을 위한 모델 검사 도구를 포함하고 있으며, 모델에 포함된 데이터 위에 술어를 표현하기 위해 형식화된 변수와 식을 사용하여 확장된다.이 확장은 표준 mu-mulus에서 표현할 수 없는 특성(예를 들어, 주어진 변수의 값이 항상 실행 경로를 따라 증가한다는 사실)을 제공한다.
이러한 기술은 효율적이고 자동화되어 있지만, 컴퓨터 메모리에 맞지 않는 모델이 너무 클 때 발생하는 국가 폭발 문제가 주된 한계점이다.CADP는 두 가지 보완적인 방법으로 모델을 처리하기 위한 소프트웨어 기술을 제공한다.
- 소형 모델은 메모리에 모든 상태와 전환(과도한 검증)을 저장하여 명시적으로 표현할 수 있다.
- 검증에 필요한 모델 상태 및 전환(즉시 검증)만 탐색하여 대형 모델을 암묵적으로 표현한다.
언어 및 컴파일 기술
신뢰할 수 있고 복잡한 시스템의 정확한 사양에는 실행 가능한 언어(열람적 검증을 위한)가 필요하며 형식적인 의미론(설계자와 구현자 사이의 해석 분산을 초래할 수 있는 언어 모호성)이 있다.형식 의미론도 무한 시스템의 정확성을 확립할 필요가 있을 때 필요하다. 이는 한정된 추상화만을 다루기 때문에 열거적 기법을 사용할 수 없기 때문에, 형식 의미론을 가진 언어에만 적용되는 정리 증명 기법을 사용해야 한다.
CADP는 시스템에 대한 LOTO 설명에 따라 작동한다.로토스는 프로세스 알헤브라스(특히 CCS와 CSP, 대수적 추상 데이터 유형)의 개념을 결합한 프로토콜 기술(ISO/IEC 표준 8807:1989)의 국제 표준이다.따라서, LOTOS는 비동기 동시 프로세스와 복잡한 데이터 구조를 모두 설명할 수 있다.
로토스는 2001년에 대폭 개정되어, 보다 뛰어난 표현력(예를 들어 실시간 제약이 있는 시스템을 기술하는 정량적 시간을 도입함으로써)을 제공하고자 하는 E-LOTOS(Enhanced-Lotos, ISO/IEC 표준 15437:2001)를 발행하게 되었다.
CADP 도구를 검증에 사용할 수 있도록 다른 프로세스 캘커리 또는 중간 형식의 설명을 LOTO로 변환하기 위해 여러 도구가 존재한다.
라이센싱 및 설치
CADP는 대학과 공공연구센터에 무료로 배포된다.업계 사용자는 한정된 기간 동안 비상업적 사용을 위한 평가 라이센스를 취득할 수 있으며, 그 이후에는 정식 라이센스가 필요하다.CADP 사본을 요청하려면 다음 위치에서 등록 양식을 작성하십시오.[3]사용권 계약이 체결된 후에는 CADP 다운로드 및 설치 방법에 대한 세부 정보가 제공된다.
도구 요약
도구 상자에는 다음과 같은 몇 가지 도구가 포함되어 있다.
- CASERS.ADT는[4] LOTOS 추상 데이터 유형을 C 유형과 C 함수로 변환하는 컴파일러다.번역에는 패턴 매칭 컴파일 기법과 통상적인 유형(정수자, 열거자, 튜플 등)의 자동인식이 최적으로 구현된다.
- CASERS는[5] LOTOS 프로세스를 C 코드(신속 프로토타이핑 및 테스트용) 또는 유한 그래프(검증용)로 변환하는 컴파일러다.번역은 몇 가지 중간 단계를 사용하여 이루어지는데, 그 중 타이핑된 변수, 데이터 처리 기능, 원자 전환으로 확장된 페트리 네트의 구축이 그것이다.
- OPEN/CASAR는 즉시 그래프를 탐색하는 도구(예: 시뮬레이션, 검증 및 테스트 생성 도구)를 개발하기 위한 일반적인 소프트웨어 환경이다.그러한 도구는 특정한 상위 언어와는 독립적으로 개발될 수 있다.이 점에서 OPEN/CASAR는 언어 지향 도구를 모델 지향 도구와 연결함으로써 CADP에서 중심적인 역할을 한다.OPEN/CASAR는 다음과 같은 프로그래밍 인터페이스를 가진 16개의 코드 라이브러리로 구성된다.
- 여러 해시함수를 포함하는 Caiser_Hash
- 순식간에 부울 방정식 시스템을 해결하는 시저_솔브
- Caiser_Stack, 깊이 우선 탐색 스택 구현
- 상태, 전환, 라벨 등의 표를 취급하는 Caiser_Table.
OPEN/CASAR 환경 내에서 많은 도구가 개발되었다.
- BISIMULTER, BISIMULTER, 이등분율 확인
- 즉석 안정 상태 시뮬레이션을 수행하는 CAPTATER
- 정상, 확률론 또는 확률론적 시스템에서 확률론적 비결정론을 제거하는 결정자
- 총판, 여러 대의 기계를 사용하여 도달 가능한 상태의 그래프를 생성함
- Evaluator(평가자), 정규 교대 없는 무적분법 공식 평가
- 코드의 임의 실행을 수행하는 실행자
- 주어진 정규식과 일치하는 실행 시퀀스를 검색하는 EXIVENITITOR
- 도달 가능한 상태의 그래프를 구성하는 제너레이터
- 도달 가능성 분석의 실현 가능성을 예측하는 예측 변수,
- 통신 시스템의 추상화를 계산하는 프로젝터
- REVENCTOR, 도달 가능한 상태의 그래프를 구성 및 최소화하는 다양한 동등성 관계
- 인터랙티브 시뮬레이션을 허용하는 시뮬레이터, X-SIMulator 및 OCIS
- 교착 상태를 검색하는 TELINGER
- BCG(Binary Coded Graphs)는 매우 큰 그래프를 디스크에 저장하기 위한 파일 형식이며(효율적인 압축 기법을 사용), 분산 처리를 위한 분할 그래프를 포함하여 이 형식을 처리하기 위한 소프트웨어 환경이다.BCG는 또한 많은 도구들이 입력/출력에서 이 형식에 의존하기 때문에 CADP에서 핵심적인 역할을 한다.BCG 환경은 프로그래밍 인터페이스가 있는 다양한 라이브러리와 다음을 포함한 여러 도구로 구성된다.
- 그래프의 2차원 뷰를 구축하는 BCG_DROW,
- Bcg_Draw에서 생성된 그래프 레이아웃을 대화형으로 수정할 수 있는 BCG_EDIT
- BCG_GRAPH, 다양한 형태의 실질적으로 유용한 그래프를 생성함
- 그래프에 대한 다양한 통계 정보를 표시하는 BCG_INFO
- BCG_IO, BCG와 기타 여러 그래프 형식 간의 변환 수행
- BCG_LABELS, 그래프의 전환 레이블을 숨기거나 이름을 변경(정규 표현식 사용)
- 분산 그래프 구성에서 얻은 그래프 조각을 수집하는 BCG_MERGE
- BCG_MIN, 그래프 모듈로 강하거나 분기하는 동등성(확률적이고 확률적인 시스템도 다룰 수 있음)을 최소화한다.
- BCG_STEDY, 연속 시간 Markov 체인에 대한 (확장) 정상 상태 수치 분석을 수행한다.
- BCG_TRANSIENT(확장된) 연속 시간 Markov 체인에 대한 일시적인 수치 분석을 수행하는 경우
- 분할된 BCG 그래프를 복사하는 PBG_CP
- 분할된 BCG 그래프에 대한 정보를 표시하는 PBG_INFO
- 분할된 BCG 그래프를 이동하는 PBG_MV
- 분할된 BCG 그래프를 제거하는 PBG_RM
- XTL(EXecable Temporary Language)은 BCG 그래프에 탐색 알고리즘을 프로그래밍하기 위한 높은 수준의 기능 언어다.XTL은 상태, 전환, 라벨, 후속 및 이전 기능 등을 처리할 수 있는 기본 기능을 제공한다.예를 들어, 통상적인 시간 로직(HML,[7] CTL,[8] ACTL [9]등)에 대한 XTL 평가 및 진단 생성 고정 지점 알고리즘에 지정할 수 있는 상태 집합의 재귀 기능을 정의할 수 있다.
명시적 모델(BCG 그래프 등)과 암묵적 모델(즉시 조사) 사이의 연결은 다음과 같은 OPEN/CASAR 호환 컴파일러에 의해 보장된다.
- CASERS.Open, 로토스 설명으로 표현된 모델용
- BCG.OPEN, BCG 그래프로 표시된 모형의 경우
- EXP.OPEN, 통신 자동화로 표현된 모델용
- FSP.OPEN, FSP 설명으로 표현되는 모델의 경우
- LNT.OPEN, LNT 설명으로 표현되는 모델의 경우
- SEQ.OPEN, 실행 트레이스 세트로 표시되는 모델의 경우
또한 CADP 도구상자에는 Verimag 실험실(그르노블)과 INRIA 렌즈의 정점 프로젝트-팀에서 개발한 ALDEBARAN과 TGV(검증에 기초한 테스트 생성)와 같은 추가 도구가 포함되어 있다.
CADP 도구는 잘 통합되어 있으며 EUCALYPTUS 그래픽 인터페이스 또는 SVL[10] 스크립팅 언어를 사용하여 쉽게 액세스할 수 있다.EUCALYPTUS와 SVL 모두 필요할 때마다 파일 형식 변환을 자동으로 수행하고 도구가 호출될 때 적절한 명령줄 옵션을 제공함으로써 사용자가 CADP 도구에 쉽고 균일하게 액세스할 수 있도록 한다.
수상
- 2002년에 CADP의 Evaluator 모델 체커를 설계하고 개발한 Radu Mateescu는 Foundation Rhne-Alpes Future가 주관하는 연례 심포지엄 10번째 판에서 귀속된 정보 기술상을 받았다.[11]
- 2019년 프레데릭 랭과 프랑코 마잔티는 CADP를 활용해 통신 상태기계의 다양한 세트에서 360도 계산 트리 논리(CTL)와 선형 시간 논리(LTL) 공식을 성공적이고 정확하게 평가해 RERS 도전의 평행 문제에서 모든 금메달을 획득했다.[13][14]
- 2020년 프레데릭 랭, 프랑코 마잔티, 웬델린 세르웨는 '병렬 CTL' 문제의 88%를 정확하게 풀어 RERS2020 챌린지에서 3관왕에 올라 90점 만점에 11개 공식에 대해 '모른다'는 답변만 했다.[15][16][17]
- 2021년에는 휴버트 개러벨, 프레데릭 랭, 라두 마테스쿠, 웬델린 세르베가 공동으로 CADP 툴박스의 개발을 이끈 과학 업적으로 인리아 혁신상 – 아카데미에 데스 과학상 – 다쏘 시스테메스를 수상했다.[18]
참고 항목
참조
- ^ Garavel H, Lang F, Mateescu R, Serwe W: CADP 2011: 기술 이전용 소프트웨어 도구 국제 저널, 15(2):89-107, 2013년 4월
- ^ ISO 8807, 시간 순서 지정 언어
- ^ CADP 온라인 요청 양식.아마존닷컴(2011-08-30).2014-06-16에 검색됨
- ^ H. 가라벨.LOTOS 추상 데이터 유형 편집, FORTE'89(Vancouver B.C., 캐나다), S. T. Vuong(편집자), North-Holland, 1989년 12월, 페이지 147–162.
- ^ H. 가라벨, J. 시파키스.제10차 국제심포지엄(캐나다 오타와), L. 로그리포, R. L. 프로버트, H. 우랄(편집자), North-Holland, IFIP, 1990년 6월 페이지 379–394의 작성 및 검증.
- ^ H. 가라벨.오픈/케이블SAR: TACAS'98(포르투갈 리스본, B), 베를린, B의 시스템 구축 및 분석을 위한 도구 및 알고리즘에 관한 제1차 국제회의의 진행에서 검증, 시뮬레이션 및 테스트를 위한 개방형 소프트웨어 아키텍처.Steffen(편집자), 컴퓨터 과학 강의 노트, 인리아 연구 보고서 RR-3352, Springer Verlag, 1998년 3월, vol. 1384, 페이지 68–84로 풀 버전을 이용할 수 있다.
- ^ M. Hennessy, R. Milner.비결정성과 동시성을 위한 대수법, in: ACM, 1985, vol. 32, 페이지 137–161.에서.
- ^ E. M. Clarke, E. A. Emerson, A. P. Sistla.시간 논리 규격을 사용한 유한 상태 동시 시스템의 자동 검증, in: 프로그래밍 언어 및 시스템에 대한 ACM 트랜잭션, 1986년 4월, vol. 8, no. 2, 244–263.
- ^ F. W. Vandrager, R. De Nicola.전환 시스템을 위한 Action 대 State Based Logics, Computer Science의 강의 노트, Springer Verlag, 1990, vol. 469, 페이지 407–419.
- ^ H. Garavel, F. Lang.SVL: 구성 검증을 위한 스크립팅 언어, in: 제21회 IFIP WG 6.1 국제 네트워크 및 분산 시스템 FORTE'2001(제주도, 한국), M. Kim, B.의 공식 기술 회의 진행.친, S. Kang, D.리(편집자), 인리아 연구 보고서 RR-4223, 클루워 학술 출판사, IFIP, 2001년 8월 페이지 377–392로 풀 버전을 이용할 수 있다.
- ^ "Radu Mateescu wins the IT Award granted by Fondation Rhône-Alpes Futur".
- ^ Isabelle Bellin (16 April 2011). "Hubert Garavel received the Gay-Lussac Humboldt Research Award". Archived from the original on 2016-07-10.
- ^ "Results of the RERS Challenge 2019".
- ^ "The CADP Newsletter Nr. 12 - April 10, 2019".
- ^ "Results of the RERS Challenge 2020".
- ^ "CNR-Inria Team Wins Gold Medals at the RERS 2020 Parallel CTL Challenge".
- ^ "The CADP Newsletter Nr. 13 - February 22, 2021".
- ^ "The Convecs team strengthens the security of parallel systems".
