TAPAs 모델 체커

TAPAs model checker

TAPAS는 동시 시스템을 지정하고 분석하기 위한 도구입니다.그것의 목적은 과정 대수의 가르침을 지원하는 것이다.시스템은 프로세스 대수 용어로 설명되며, 이후 라벨이 부착된 전이 시스템(LTS)에 매핑됩니다.특성은 구체적인 시스템 설명과 추상 시스템 설명 간의 동등성을 확인하거나 획득한 LTS에 대한 시간 공식(μ-calculus 또는 ACTL로 표현)을 모델 확인함으로써 검증할 수 있습니다.특히 교육에 적합한 TAPA의 주요 특징은 각 시스템의 일관된 그래픽 및 텍스트 표현을 유지하는 것입니다.그래픽 표기가 변경된 후에는 텍스트 표현이 즉시 업데이트되지만 텍스트 수정 후에는 그래픽 표현의 업데이트가 수동으로 트리거되어야 합니다.

TAPA에서 동시 시스템은 시스템 동작을 비결정적으로 기술하는 프로세스와 프로세스 구성에 의해 취득되는 프로세스 시스템에 의해 기술됩니다.특히 프로세스는 다른 프로세스 또는 프로세스 시스템의 관점에서 정의할 수 있습니다.프로세스 및 프로세스 시스템은 주어진 프로세스 대수의 연산자를 사용하여 구성된다.현재 TAPA는 CCSP와 PEPA의 두 가지 프로세스 대수를 지원합니다.

CCSP(= CCS + CSP)는 CSP의 일부 운영자를 고려하여 CCS에서 얻습니다.CCSP 프로세스 시스템을 작성한 후 사용자는 다음 도구 중 하나를 사용하여 분석할 수 있습니다.

  • Equivalence Checker: 등가(이중 시뮬레이션, 분기 이중 시뮬레이션 또는 장식된 트레이스)를 사용하여 자동 데이터 쌍을 비교할 수 있습니다.
  • 모델 검사기: 시스템 모델이 지정된 사양에 부합하는지 자동으로 테스트합니다.
  • 시뮬레이터: 시스템을 통해 가능한 실행 경로를 추적하여 사용자에게 실행 추적을 제공합니다.

PEPA(Performance Evaluation Process Algebra)는 Jane Hillston이 1990년대에 도입한 컴퓨터와 통신 시스템을 모델링하기 위해 설계된 확률적 프로세스 대수입니다.이 언어는 확률론적 분기 및 전환 타이밍을 도입함으로써 밀너의 CCS 및 호어의 CSP와 같은 고전적인 프로세스 대수학을 확장한다.속도는 지수 분포에서 도출되며 PEPA 모델은 유한 상태이므로 확률적 과정, 특히 연속 시간 마르코프 과정(CTMC)을 발생시킨다.따라서 이 언어는 처리량, 이용률, 응답시간과 같은 컴퓨터 및 통신 시스템 모델의 양적 특성과 교착상태로부터의 해방과 같은 질적 특성을 연구하는 데 사용될 수 있다.언어는 고든 플롯킨이 발명한 스타일의 구조화된 운영 의미론을 사용하여 공식적으로 정의된다.

TAPAS는 1990년 Pisa의 IEI CNR에 의해 JACK이라는 이름의 도구로 시작된 집단 작업의 결과입니다.이 작업은 피사의 ISTI-CNR에 의해 계속되었다.새로운 TAPA 버전은 플로렌스 대학의 Dipartimento Sistemi ed Informatica에서 개발되었습니다.

「 」를 참조해 주세요.

레퍼런스

외부 링크