Rebeca(프로그래밍 언어)
Rebeca (programming language) |
Rebeca(Reactive Objects Language를 위한 Acronym)는 공식 기반 배우 기반 모델링 언어로, 공식 검증 접근 방식과 실제 애플리케이션 간의 격차를 해소하기 위해 설계되었습니다.행위자 모델의 연산 해석에 기초한 동시 연산을 위한 참조 모델로 간주할 수 있다.또한 실제로 객체 기반 동시 시스템을 개발하기 위한 플랫폼이기도 합니다.
동시에 분산된 시스템을 모델링하기 위한 적절하고 효율적인 방법이 있을 뿐만 아니라 정확성을 보장하기 위한 공식적인 검증 접근법이 필요합니다.Rebeca는 일련의 검증 도구에서 지원됩니다.이전의 툴은, Rebeca 코드로 동작하는 프런트 엔드를 제공해, Rebeca 코드를 잘 알려진 성숙한 모델 체커(SPIN이나 NuSMV 등)의 입력 언어로 변환해, 그 속성을 검증할 수 있었습니다.2005년 이후, Rebeca는 Modere(Rebeca의 Model Checking Engine) 기반의 직접 모델 체커에 의해 지원되고 있습니다.모듈러 검증 및 추상화 기술은 상태 공간을 줄이고 복잡한 반응 시스템을 검증할 수 있도록 하기 위해 사용됩니다.이러한 기술 외에도 Modere는 부분 차수 감소 및 대칭 축소를 지원합니다.
「 」를 참조해 주세요.
레퍼런스
- M. 시르자니2004년 12월 샤리프 공과대학 컴퓨터공학과 박사논문, 동시 및 반응 시스템의 정식 사양 및 검증.
- M. 시르자니, A.모바가르2002년 10월 오스트리아 컴퓨터 학회 정보 관리 에이전트에 관한 워크숍의 진행에 있어서의 에이전트 대상 모델.
외부 링크
