우파알 모델 체커
Uppaal Model Checker| 개발자 | 웁살라 대학교 알보르 대학교 |
|---|---|
| 초기 릴리즈 | 1995 |
| 안정적 해제 | 4.0.14 / 2014년 5월 20일; 전 |
| 릴리스 미리 보기 | 4.1.22 / 2019년 3월 28일; 전 |
| 기록 위치 | Java의 C++ 및 GUI |
| 운영 체제 | 리눅스 맥 OS X 마이크로소프트 윈도 |
| 다음에서 사용 가능 | 영어 덴마크어 일본인입니다 중국어 리투아니아어 |
| 유형 | 모델체크 |
| 면허증 | 상용 라이선스 학술 자격증 |
| 웹사이트 | http://www.uppaal.org/ http://www.uppaal.com/ |
UPAAL은 데이터 유형(경계 정수, 어레이 등)으로 확장되고, 타임오토마타 네트워크로 모델링된 실시간 시스템의 모델링, 검증 및 검증을 위한 통합 툴 환경이다.
1995년 출시한 레고 마인드스톰, 필립스 오디오 프로토콜, 메셀용 변속 장치 컨트롤러 등 최소 17건의 사례연구에 활용됐다.[1]
이 도구는 스웨덴 웁살라 대학교의 실시간 시스템 그룹 설계 및 분석과 덴마크의 알보르 대학교의 컴퓨터 과학 기초 연구 사이에 공동으로 개발되었다.
사용할 수 있는 확장자는 다음과 같다.
- 비용 최적 도달 가능성 분석을 위한 코라.
- 실시간 테스트용 트론 온라인 시스템(블랙박스 적합성 테스트)
- 커버리지-최적 오프라인 테스트 생성을 위한 커버.
- Tiga for TImed GAmes based 컨트롤러 합성.
- 부분 주문 감소 기법을 활용하는 구성 요소 기반 타이밍 시스템용 포트.
- PROBabilistic 도달 가능성 분석용 프로.(계속)
- SMC 통계 모델 검사.
참조
외부 링크
