프리즘 모델 체커
PRISM model checkerPRISM은 확률론적 [1][2]행동을 보이는 시스템의 모델링 및 분석을 위한 공식 검증 소프트웨어 도구인 확률론적 모델 검사기입니다.이러한 시스템의 한 가지 소스는 블루투스 및 FireWire와 같은 통신 프로토콜이나 크라우드 및 양파 라우팅과 같은 보안 프로토콜에서 랜덤화를 사용하는 것입니다.확률적 동작은 많은 다른 컴퓨터 시스템에서도 발생합니다. 예를 들어, 기기 고장이나 예측할 수 없는 통신 지연으로 인해 발생합니다.그러나 이런 종류의 분석에 적응할 수 있는 또 다른 종류의 시스템은 생화학 반응 네트워크이다.
PRISM은 이산 시간 마르코프 연쇄, 연속 시간 마르코프 연쇄, 마르코프 의사결정 과정 및 시간 자동 형식주의의 확률론적 확장을 포함한 여러 가지 유형의 확률론적 모델을 분석하는 데 사용될 수 있다.이러한 모델에 대해 검증해야 할 특성은 시간 논리의 확률론적 확장으로 표현된다.
PRISM의 개발은 주로 버밍엄 대학과 옥스퍼드 대학에서 이루어집니다.이 도구는 오픈 소스 소프트웨어이며 GNU General Public License에 따라 출시됩니다.PRISM은 2013년과 2014년에 Google Summer of Code 프로그램에 선정되었습니다.
레퍼런스
- ^ 퀴아트코프스카, M., 노먼, G., 파커, D. (2011년)"PRISM 4.0: 확률론적 실시간 시스템 검증"제23회 컴퓨터 지원 검증 국제회의(CAV'11), 컴퓨터 과학 강의 노트 6806권, 585-591쪽, 스프링거.
- ^ Kwiatkowska, M.; Norman, G.; Parker, D. "실행 중인 확률론적 모델 확인:PRISM을 사용한 도입 사례.". ACM SIGMETRICS 퍼포먼스 평가 리뷰, 32(4), 16~21페이지.
외부 링크
