도달성 분석

Reachability analysis

도달 가능성 분석은 분산 시스템의 특정한 맥락에서 도달 가능성 문제에 대한 해결책이다.메시지 교환에 의해 통신하는 일정 수의 지역 실체로 구성된 분산 시스템에 의해 어떤 글로벌 상태에 도달할 수 있는지 결정하는 데 사용된다.null

개요

도달 가능성 분석은 통신 프로토콜의 분석과 검증을 위해 1978년 논문에 도입되었다.[1]본 논문은 프로토콜 실체의 유한 상태 모델링을 이용한 교대 비트 프로토콜을 제시한 1968년의 바틀렛 외 연구원의 논문에서 영감을 받았으며, 앞서 설명한 유사한 프로토콜이 설계 결함을 가지고 있다는 점도 지적했다.이 프로토콜은 링크 계층에 속하며, 특정한 가정 하에서, 메시지 손상이나 손실이 가끔 존재함에도 불구하고 손실이나 중복이 없는 정확한 데이터 전달을 서비스로서 제공한다.null

도달 가능성 분석의 경우, 지역 실체는 상태 및 전환에 의해 모델링된다.기업은 메시지를 보내거나, 받은 메시지를 소비하거나, 로컬 서비스 인터페이스에서 상호작용을 수행할 때 상태를 변경한다.The global state of a system with n entities [3] is determined by the states (i=1, ... n) of the entities and the state of the communication .가장 간단한 경우, 두 실체 사이의 매체는 (보냈지만 아직 소비되지 않은) 전송 중인 메시지를 포함하는 반대 방향으로 두 FIFO 대기열에 의해 모델링된다.도달 가능성 분석은 실체들의 가능한 상태 전환의 모든 시퀀스들을 분석함으로써 분산 시스템의 가능한 행동을 고려하며, 해당 글로벌 상태에 도달했다.[4]null

도달 가능성 분석의 결과는 초기 글로벌 상태에서 도달할 수 있는 분산 시스템의 모든 글로벌 상태와 지역 실체가 수행하는 모든 송신, 소비 및 서비스 상호작용의 가능한 시퀀스를 보여주는 글로벌 상태 전환 그래프(접근성 그래프라고도 함)이다.그러나, 많은 경우에 이 전환 그래프는 한이 없고 완전히 탐색할 수 없다.전환 그래프는 프로토콜의 일반적인 설계 결함(아래 참조)을 확인하는 데 사용할 수 있지만, 또한 각 기업에 의한 서비스 상호작용의 순서가 시스템의 글로벌 서비스 규격에 의해 제시된 요건에 부합하는지 검증하는 데도 사용할 수 있다.[1]null

프로토콜 속성

경계:글로벌 상태 전환 그래프는 전송될 수 있는 메시지 수가 제한되고 모든 엔터티의 수 상태가 제한되는 경우 제한된다.유한 상태 실체의 경우 메시지의 수가 경계를 유지하는지 여부는 일반적으로 결정 가능하지 않다.[5]일반적으로 전송 중인 메시지 수가 지정된 임계값에 도달하면 전환 그래프의 탐색을 잘라낸다.null

다음은 설계 결함이다.

  • 글로벌 교착 상태:모든 실체가 메시지 소비를 기다리며 메시지가 전송되지 않으면 시스템은 전 세계적인 교착 상태에 빠져 있다.글로벌 교착상태의 부재는 도달성 그래프에 어떤 상태도 글로벌 교착상태인지 확인함으로써 확인할 수 있다.
  • 부분 교착 상태:기업이 메시지의 소비를 기다리고 시스템이 그러한 메시지가 전송되지 않는 글로벌 상태에 있고 미래에 도달할 수 있는 어떤 글로벌 상태에서도 결코 전송되지 않을 경우 기업은 교착상태에 빠져 있다.이러한 국부적이지 않은 속성은 도달 가능성 그래프에서 모델 확인을 수행하여 확인할 수 있다.
  • 지정되지 않은 수신:다음 소비할 메시지가 현재 상태의 기업의 행동규격으로 예상되지 않는 경우 기업은 지정되지 않은 수신을 하게 된다.이 조건의 부재는 도달성 그래프의 모든 상태를 확인함으로써 확인할 수 있다.

예

도표는 두 개의 프로토콜 실체와 그들 사이에 교환된 메시지를 보여준다.
도표는 각각의 프로토콜 실체의 동적 동작을 정의하는 두 개의 유한 상태 기계를 보여준다.
이 도표는 두 개의 프로토콜 실체와 그들 사이의 메시지 교환에 사용되는 두 개의 FIFO 채널로 구성된 글로벌 시스템의 상태 기계 모델을 보여준다.

예를 들어, 우리는 첫 번째 다이어그램에서와 같이 ma, mb, mc, md 메시지를 서로 교환하는 두 개의 프로토콜 실체의 시스템을 고려한다.프로토콜은 두 실체의 동작에 의해 정의되는데, 두 번째 도표는 두 개의 상태 기계 형태로 주어진다.여기서 "!"라는 기호는 메시지를 보내는 것을 의미하고, "?"는 수신된 메시지를 소비하는 것을 의미한다.초기 주는 주 "1"이다.

세 번째 도표는 이 프로토콜에 대한 도달 가능성 분석의 결과를 글로벌 상태 기계의 형태로 보여준다.각 글로벌 상태에는 프로토콜 실체 A의 상태(왼쪽), 실체 B의 상태(오른쪽) 및 중간 전달 메시지(상단 부분: A에서 B로, 하단 부분: B에서 A로)의 네 가지 구성요소가 있다.이 글로벌 상태 시스템의 각 전환은 프로토콜 엔터티 A 또는 엔터티 B의 하나의 전환에 해당한다.초기 상태는 [1, - , 1](전송 중 메시지 없음)이다.null

한 사람은 이 예가 경계된 글로벌 상태 공간을 가지고 있다고 본다 - 동시에 전송될 수 있는 최대 메시지 수는 두 개일 수 있다.이 프로토콜은 [2, - , 3] 상태인 글로벌 교착 상태를 가지고 있다.메시지 mb를 소비하기 위해 상태 2에서 A의 전환을 제거하면 [2, ma mb ,3], [2, -mb ,3], [2, -mb ,3] 글로벌 상태에서 지정되지 않은 수신이 있게 된다.null

메시지 전송

프로토콜의 설계는 기초적인 통신매체의 속성, 통신파트너가 실패하는 가능성, 그리고 기업이 소비할 다음 메시지를 선택하기 위해 사용하는 메커니즘에 맞게 수정되어야 한다.링크 수준의 프로토콜에 대한 통신 매체는 일반적으로 신뢰할 수 없으며 잘못된 수신과 메시지 손실을 허용한다(매체의 상태 전환으로 모델링됨).인터넷 IP 서비스를 이용하는 프로토콜은 또한 고장난 배달의 가능성을 다루어야 한다.상위 수준의 프로토콜은 일반적으로 세션 지향 전송 서비스를 사용하며, 이는 매체가 어떤 한 쌍의 엔티티 간에 신뢰할 수 있는 FIFO의 메시지 전송을 제공한다는 것을 의미한다.그러나 분산 알고리즘 분석에서는 일부 실체가 완전히 실패할 가능성을 고려하는 경우가 많으며, 이는 일반적으로 예상 메시지가 도착하지 않을 때 타임아웃 메커니즘에 의해 감지된다(매체의 메시지 손실처럼).null

여러 메시지가 도착하여 소비 준비가 되었을 때 특정 메시지를 소비용으로 선택할 수 있는지에 대해 서로 다른 가정을 해왔다.기본 모델은 다음과 같다.

  • 단일 입력 대기열:각 엔터티는 하나의 FIFO 대기열을 가지고 있으며, 수신 메시지가 소비될 때까지 저장된다.여기서 기업은 선택권이 없으며 큐의 첫 번째 메시지를 소비해야 한다.
  • 다중 대기열:각 엔티티에는 통신 파트너당 하나씩 여러 개의 FIFO 대기열이 있다.여기서 기업은 그 상태에 따라 다음 입력 메시지를 소비할 대기열(또는 대기열)을 결정할 수 있다.
  • 수신 풀:각 엔터티는 수신된 메시지가 소비될 때까지 저장되는 단일 풀을 가지고 있다.여기서 기업은 상태에 따라 다음에 어떤 유형의 메시지를 소비해야 하는지(그리고 아직 메시지가 수신되지 않은 경우 메시지를 기다리거나) 결정하거나 일련의 메시지 유형에서 (대안을 처리하기 위해) 하나를 소비할 수 있는 힘을 갖는다.

지정되지 않은 수신의 문제를 식별하는 원본 논문과 [6]후속 작업의 상당 부분은 단일 입력 대기열을 가정했다.[7]때때로, 지정되지 않은 리셉션이 경주 조건에 의해 도입되기도 하는데, 이는 두 개의 메시지가 수신되고 그 순서가 정의되지 않는다는 것을 의미한다(다른 파트너로부터 온다면 종종 그러하다).이러한 설계 결함의 대부분은 여러 대기열 또는 수신 풀을 사용할 때 사라진다.[8]수신 풀을 체계적으로 사용하여 도달 가능성 분석을 통해 부분적인 교착 상태와 메시지가 풀에 영구히 남아 있는지 확인해야 한다(기업이 소비하지 않음).

실무문제

프로토콜 모델링에 관한 대부분의 작업은 분산된 실체의 행동을 모델링하기 위해 유한 상태 기계(FSM)를 사용한다(또한 유한 상태 기계 전달 참조).그러나 이 모델은 메시지 매개변수와 로컬 변수를 모델링할 만큼 강력하지 않다.따라서 SDL이나 UML 상태 기계와 같은 언어에서 지원하는 것과 같이 소위 확장 FSM 모델이 종종 사용된다.불행히도 그러한 모델의 경우 도달 가능성 분석이 훨씬 더 복잡해진다.null

도달 가능성 분석의 실제적인 문제는 이른바 ″상태 공간 폭발이다.프로토콜의 두 실체가 각각 100개의 상태를 가지고 있고, 매체가 각 방향에서 최대 2개의 메시지를 포함할 수 있는 경우, 도달성 그래프에서 글로벌 상태의 수는 100 x 100 x (10 x 10) x (10 x 10) x (10 x 10)의 숫자 100 x 100 x (10 x 10) x (10 x 10)로 제한된다.따라서 도달성 그래프에서 자동으로 도달성 분석 및 모델 확인을 수행할 수 있는 여러 도구가 개발되었다.두 가지 예만 언급한다.SPIN 모델 체커와 분산 공정의 구축 및 분석을 위한 툴박스.null

추가 읽기

참조 및 참고 사항

  1. ^ a b Bochmann, G.v. "Finite State Description of Communication Protocols, Computer Networks, Vol. 2 (1978), pp. 361-372". {{cite journal}}:Cite 저널은 필요로 한다. journal=(도움말)
  2. ^ K.A. Bartlett, R.A. Scantlebury and P.T.Wilkinson, 하프 듀플렉스 링크에 대한 신뢰성 있는 전이중 전송에 관한 노트, C.ACM 12, 260(1969년).
  3. ^ 참고: 프로토콜 분석의 경우 일반적으로 두 개의 실체만 존재한다.
  4. ^ 참고: 메시지의 손상 또는 상실은 m m 의 상태 전환으로 모델링
  5. ^ M.G.고우다, E.G.매닝, Y.T.유: 두 유한한 상태 기계 사이의 의사소통의 진행에 관하여, 도이
  6. ^ P. 자피로풀로, C.웨스트, H. 루딘, D.Cowan, D. Brand : 프로토콜 분석과 합성을 위해 IEEE Transactions on Communications (제28권, 제4권, 1980년 4월)
  7. ^ 참고: SDL의 SAVE 구성을 사용하여 특정 유형의 메시지를 현재 상태에서 소비하지 말고 향후 처리를 위해 저장해야 함을 나타낼 수 있다.
  8. ^ M.F. 알함무리와 G.v. 보흐만 : 서비스 규격의 실현 가능성, Proc.시스템 분석 및 모델링(SAM) 회의 2018, 코펜하겐, LNCS, 스프링거
  9. ^ C. 포넷, T.Hoare, S. K. Rajamani, J. Lehof : 고착 없는 순응, Proc. 16번째 Intl.컴퓨터 보조 검증(CAV'04), LNCS, vol. 3114, Springer, 2004에 관한 설명