모델 점검 도구 목록

List of model checking tools

이 글은 모델 점검 도구를 나열하고 각 기능의 개요를 제공한다.

일부 모델 점검 도구 개요

다음 표에는 다음과 같은 기능이 있는 모델 체커가 포함되어 있다.

(1) 다운로드할 수 있는 웹 사이트,

(2) 신고된 면허,

(3) 보관된 문헌에 게재된 설명 및

(4) 이를 설명하는 위키백과 기사.

아래 표에서는 다음과 같은 약어가 사용된다.

  • 동등성:
    • SB: 강한 비시뮬레이션
    • WB: 약한 비시뮬레이션
    • BB: 분기 비시뮬레이션
    • STE: 강력한 추적 동등성
    • WTE: 약한 추적 동등성
    • 나: 메이 동등성
    • ME: Must Equality
    • OE: 관측 동등성
    • SE: 안전 동등성
    • t*E: tau*.a 동등성
  • 소프트웨어 라이센스:
    • FURIC: 특정 조건 하에서 무료(예: 학업에 대한 무료)
이름 모델 검사 동등성 검사 GUI 유용성
평범함, 확률론, 확률론, ... 모델링 언어 속성 언어 지원되는 동등성 카운터 예제 생성 GUI 그래픽 사양 카운터 예제 시각화 소프트웨어 라이선스 사용된 프로그래밍 언어 플랫폼/OS
블라스트 코드분석 C 모니터오토마타 네 아니요. 아니요. 아니요. 무료 OCAML Windows 및 Unix 관련
CADP 일반 및 확률론 로토스, FC2, FSP, LNT AFMC, MCL, XTL SB, WB, BB, OE, STE, WTE, SE, tau*E 네 네 아니요. 네 FUSIC C, 본 쉘, Tcl/Tk, LOTOS, LNT Mac OS, Linux, Solaris, Windows
CPA체커 코드분석 C 모니터오토마타 네 네 아니요. 네 무료 자바 아무거나
드림 실시간 C++, 시간 지정 자동 기록 모니터오토마타 네 아니요. 아니요. 아니요. 무료 C++ Windows 및 Unix 관련
자바 패스파인더 일반 및 시간 제한 자바 알 수 없는 아니요. 네 아니요. 아니요. 오픈 소스 계약 자바 Mac OS, Windows, Linux
LTSmin 일반, 실시간 Promela, μCRL, mCRL2, DVE 입력 언어, UPAAL 시간 자동 기록, 이벤트-B, CSP, TLA+, Z, Petri net μ-계산, LTL, CTL* SB, BB 네 아니요. 아니요. 아니요. 무료 C, C++ Unix, Mac OS X, Windows
mCRL2 일반, 실시간 mCRL2 μ-미적분 SB, BB, t*E, STE, WTE 네 네 아니요. 네 무료 C++ Mac OS, Linux, Solaris, Windows
MRMC 실시간, 확률론적 플레인 MC CSL, CSRL, PCTL, PRCTL SB 아니요. 아니요. 아니요. 아니요. 무료 C Windows, Linux, Mac OS
무르시 (머피) 플레인 무르시 불변제, 주장 네 아니요. 아니요. 아니요. 무료 C++ 리눅스
누에스엠브 플레인 SMV 입력 언어 CTL, LTL, PSL 네 아니요. 아니요. 아니요. 무료 C Unix, Windows, Mac OS X
팻 일반, 실시간, 확률론 CSP#, 시간 지정 CSP, 확률론 CSP LTL, 주장 네 네 네 네 무료 C# Windows, 다른 OS(Mono 포함)
프리즘 확률론적 PEPA, 프리즘 언어, 플레인 MC CSL, PLTL, PCTL 아니요. 네 아니요. 아니요. 무료 C++, 자바 Windows, Linux, Mac OS
SPIN 플레인 프로멜라 LTL 네 네 아니요. 네 FUSIC C, C++ Windows 및 Unix 관련
타파알 실시간 Timed-Arc Petri Nets, 연령 불변제, 억제 호, 운송 호 TCTL 부분 집합 아니요. 네 네 네 무료 C++, 자바 Mac OS, Windows, Linux
타파스 플레인 CCSP CTL, μ-미적분법 SB, WB, BB, STE, WTE, 나, ME, OE 네 네 네 네 무료 자바 Windows, Mac OS 및 Unix 관련
우파알 실시간 타이밍 설정 자동 파라미터, C 하위 집합 TCTL 부분 집합 네 네 네 네 FUSIC C++, 자바 Mac OS, Windows, Linux
로미오 실시간 타임 페트리 네트, 스톱워치 파라메트릭 페트리 네트 TCTL 부분 집합 네 네 네 아니요. 무료 C++, tcl/tk Mac OS, Windows, Linux
TLA+ Model Checker(TLC) 플레인 TLA+, PlusCal TLA 네 네 네 아니요. 무료 자바 Mac OS, Windows, Linux

모델링 언어

  • CCSP: CSP의 일부 연산자를 통합하여 CCS로부터 얻은 공정 미적분.그것은 엘더그와[1] 판 글래브벡/반란드라거에 의해 정의된다.[2]
  • CSP: 순차적 프로세스 전달, 동시 시스템에서의 상호작용 패턴을 기술하기 위한 공식 언어.FDR2는 CSP를 위한 정밀 검사 도구로, 호환성을 위해 두 모델을 비교한다.
  • DVE 입력 언어: 시스템은 공유 변수와 버퍼링되지 않은 채널을 통해 통신하는 확장 유한 상태 기계의 네트워크로 설명된다.버퍼링된 채널에 대한 지원 및 적절한 수신 수행 없이 수신할 메시지 유형을 확인하기 위한 지원이 포함되지 않음.
  • FC2: (공통 형식 V2) 자동 데이터의 동기화된(계층적) 네트워크에 대한 시스템 수준 ASCII 표현Esprit 기초 연구 활동 CONCER, 1992년에 정의되었다.주로 프로세스 알헤브라의 영역에서 다수의 검증 도구에 의해 입력 및 교환 형식으로 사용된다.
  • FSP: 임페리얼 칼리지에서 정의된 유한 상태 프로세스 언어.
  • Java: 객체 지향 프로그래밍 언어.
  • LNT: LOTOS New Technology; 프로세스 캘커리, 기능 프로그래밍 언어 및 명령 프로그래밍 언어에서 영감을 받은 사양 언어; LNT는 LOTOS와 E-LOTOS를 현대적으로 대체하기 위해 설계되었다.
  • LOTOS: 시간순 주문 명세서(ISO 표준 8807); ISO OSI 표준에서 프로토콜 명세에 사용되는 시간순 주문에 기초한 공식 사양 언어.
  • Murφ: 지킴이 명령과 비동기식 인터리빙 동시성 모델이며, 모든 동기화 및 통신은 글로벌 변수를 통해 이루어진다.
  • PEPA: 성능평가 과정 대수학; 컴퓨터 및 통신 시스템을 모델링하기 위해 설계된 확률적 과정 대수학이다.
  • 일반 MC: MRMC와 프리즘에 사용되는 간단한 텍스트 파일 형식.
  • Promela: Process or Protocol Meta Language; 그것은 검증 모델링 언어다.언어는 예를 들어 분산형 시스템을 모델링할 동시 프로세스를 동적으로 만들 수 있도록 한다.
  • TLA+: 시간적 행동 논리를 기반으로 하는 범용 규격 언어, 원래 분산형 및 동시형 시스템에 사용되었다.규격의 언어와 그 속성은 동일하다.

속성 언어

  • AFMC: 교대-자유 모달 μ-미적분.
  • 주장:명령적 주장 성명.
  • CSL: Continuous Stochastic Logic, 연속 시간 마르코프 프로세스의 이등분화 특성.
  • CSRL: 연속 확률적 보상 논리; 보상 구조로 확장된 CTMC에 대해 조치를 명시하는 논리(일명 마르코프 보상 모델).
  • CTL: Computing Tree Logic, 즉 시간의 모델은 미래가 결정되지 않은 나무와 같은 구조라는 뜻의 분기 시간 논리; 미래에 다른 경로가 있고, 그 중 어느 것이든 실현되는 실제 경로가 될 수 있다.
  • 불변성: 시스템 상태 위에 술어가 있음.
  • LTL: 선형 시간 논리, 시간을 나타내는 모달 시간 논리.
  • MCL: Model Checking Language; Alternation-Free Modal μ-분산 사용자 친화적인 정규식과 값-통과 구조; CTL과 LTL을 소급한다.
  • mCRL2 mu-mulus: Kozen의 명제 모달 μal μ-mulus(원자 명제 제외), 확장: 데이터 변위 프로세스, 데이터 유형에 대한 정량화, 다중 작용, 시간 및 정규 공식.
  • PCTL: 확률론적 CTL, 기술된 속성의 확률론적 정량화를 허용하는 CTL의 확장.
  • PLTL: 확률론적 선형 시간 논리.
  • PRCTL: 확률론적 보상 계산 트리 논리: 보상 경계 속성으로 PCTL을 확장한다.
  • PSL: 속성 사양 언어
  • SVA: SystemVerilog 표준 어설션 언어 하위 집합, IEEE 1800으로 표준화
  • XTL: eXtended Temporary Language(eXtended Temporary Language), 조치 기반의 명시적 상태, 가치 전달 모델 체커를 신속하게 구현하기 위한 도메인별 언어.

모델 점검 도구 비교

과학 출판물

공통 사례 연구에서 다양한 모델 체커를 체계적으로 비교한 논문이 몇 개 있다.비교에서는 일반적으로 각 모델 체커의 입력 언어를 사용할 때 직면하는 모델링 트레이드오프와 정확성 특성을 확인할 때 도구의 성능 비교에 대해 논한다.언급할 수 있는 것은 다음과 같다.

  • 1999년 Judi Romijn은 가전제품용 HAVi 상호운용성 오디오-비디오 프로토콜에서 두 가지 모델 체커(CADP와 SPIN)를 비교했다.[3]
  • 2003년에는 예이피동, 샤오쿤두, 제라드 J. 홀츠만, 스콧 A.스몰카는 통신 프로토콜인 GNU i-protocol에 네 가지 모델 체커(이름: 코스판, 머피, SPIN, XMC)의 비교를 게재했다.[4]
  • 2005년에 엘레나 M.Bortnik, Nikola Trcka, Anton Wijs, Bas Luttik, J. M. van de Mortel-Fronczak, Jos C. M. Baeten, Wan Fokkink, and J. E. Rooda published a comparison of four model checkers (namely: CADP, muCRL, SPIN, and UPPAAL) on an industrial manufacturing system, a rotating drilling machine.[5]
  • 2018년 F. 마잔티와 A.Ferrari published a comparison of ten model checkers (namely: CADP, CPN Tools, FDR4, NuSMV/nuXmv, mCRL2, ProB, SPIN, TLA+, UMC, and UPPAAL) on a train supervision problem, taking into account both the user-friendliness of the languages and the performance of the tools.[6]

국제 소프트웨어 대회

공통 벤치마크

  • MCC(모델 점검 콘테스트의 모델): 많은 학술 및 산업 사례 연구에서 유래한 수백 개의 페트리 네트 모음입니다.
  • VLTS(Very Large Transition Systems): 크기가 증가하는 라벨링된 전환 시스템 모음으로, 많은 과학 간행물에 사용된다.

참조

  1. ^ E.R. Eldog: CCSP를 위한 운영 페트리 순 의미론
  2. ^ Rob van Glabbeek, Frits Vaandrager: 번들 이벤트 구조 및 CCSP
  3. ^ Romijn, Judi (June 1999). Model Checking a HAVi Leader Election Protocol (Technical report). Amsterdam: CWI. SEN-R9915. Archived from the original on 2019-09-11. Retrieved 2018-06-14.
  4. ^ Dong, Yifei; Du, Xiaoqun; Holzmann, Gerard; Smolka, Scott (2003). "Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking". Software Tool for Technology Transfer. 4 (4): 505–528.
  5. ^ Bortnik, Elena M.; Trcka, Nikola; Wijs, Anton; Luttik, Bas; van de Mortel-Fronczak, J. M.; Baeten, Jos C. M.; Fokkink, Wan; Rooda, J. E. (2005). "Analyzing a chi model of a turntable system using Spin, CADP and Uppaal" (PDF). Journal of Logical and Algebraic Methods in Programming. 65 (2): 51–104. doi:10.1016/j.jlap.2005.05.001. Archived (PDF) from the original on 2021-01-27. Retrieved 2018-05-25.
  6. ^ Mazzanti, Franco; Ferrari, Alessio (2018). "Ten Diverse Formal Models for a CBTC Automatic Train Supervision System". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation (MARS/VPT’18), Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science. Vol. 268. pp. 104–149. arXiv:1803.10324v1. doi:10.4204/EPTCS.268.4.

외부 링크

아직 위키백과 페이지가 없는 기타 모델 검사기:

그리고