FDR(소프트웨어)
FDR (software) | |
| 개발자 | 옥스퍼드 대학교 코코텍 |
|---|---|
| 안정된 릴리스 | 4.2.4 / 2019년 2월 , 전( |
| 운영 체제 |
|
| 유형 | CSP 미세화 검사기 |
| 면허증. | 독점 소프트웨어 |
| 웹 사이트 | https://cocotec.io/fdr/ |
FDR(Failures-Divergences Refinement) 및 그 후 FDR2, FDR3, FDR4는 Communicating Sequential Process(CSP; 통신 시퀀셜프로세스)에서 나타내는 정식 모델을 체크하기 위해 설계된 정제 체크 소프트웨어 도구입니다.이 툴은 원래 Formal Systems (Europe) [1]Ltd에 의해 개발되었습니다.옥스퍼드 대학 컴퓨터 과학부의 빌 로스코는 이 도구에 사용되는 많은 알고리즘을 고안했고 마이클 골드미스는[2] 구현에 [3]중요한 역할을 했습니다.FDR2는 Oxford 대학 컴퓨터 과학부에 의해 개발되었으며, 학술 및 기타 비상업적인 용도로 [4]자유롭게 사용할 수 있었습니다.
FDR은 모델체커로 기술되는 경우가 많지만 기술적으로는 미세화 체커입니다.이는 2개의 CSP 프로세스 식을 LTS(Labeled Transition System)로 변환한 후 특정 의미 모델(트레이스, 장애, 장애/분산) 내에서 프로세스 중 하나가 다른 프로세스보다 미세화되었는지 여부를 판별하기 때문입니다.ives)[5] FDR2는 프로세스 LTS에 다양한 상태 공간 압축 알고리즘을 적용하여 미세화 검사 중에 탐색해야 하는 상태 공간의 크기를 줄입니다.
FDR2는 1995년에 현재 FDR1이라고 불리는 이전 도구를 대체하여 많은 릴리즈를 거쳤습니다.FDR3는 병렬 실행 및 통합형 검사 기능을 통합한 완전히 다시 작성된 버전입니다.FDR3는 옥스포드대학에 의해 출시되며, 옥스포드대학은 2008-12년 [6]FDR2도 출시했다.ProBE CSP 애니메이터는 FDR3에 내장되어 있습니다.이것으로 FDR4가 계승했습니다.FDR4는 [7]Cocotec에서 구입할 수 있습니다.
레퍼런스
- ^ Formal Systems (유럽) Ltd.
- ^ 마이클 골드스미스 교수(현 옥스퍼드 대학의 교수이기도 하다.
- ^ 필리파 브로드풋과 빌 로스코.FDR 및 그 응용 프로그램 튜토리얼Klaus Havelund, John Penix, Willem Visser(편집자), SPIN 모델 체크 및 소프트웨어 검증, Springer-Verlag, 컴퓨터 과학 강의 노트, Volume 1885, 322 페이지, 2000.
- ^ 소프트웨어: FDR2 (상용 라이선스는 Formal Systems (Europe) Ltd에서 취득 가능)
- ^ A.W. Roscoe (1994). "Model-checking CSP". In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall.
{{cite journal}}:Cite 저널 요구 사항journal=(도움말) - ^ FDR3의 개요
- ^ 소프트웨어: FDR4 (다운로드 후 최초 시작 후 상용 라이선스 취득 가능)
