최근, 유한 상태 오토마타의 방언을 사용하여 지정된 서비스 애플리케이션을 실현하기 위해 계약 오토마타 런타임 환경(CARE)이라는 분산 미들웨어 애플리케이션이 도입되었습니다. 본 논문에서는 CARE의 형식적인 모델링, 검증 및 테스트를 상세히 설명합니다. 우리는 이를 확률적 시간 오토마타 네트워크로 형식화합니다. 모델은 원하는 속성에 대해 Uppaal 도구를 사용하여 검증되며, 철저한 및 통계적 모델 검증 기법이 활용됩니다. 추상 테스트는 CARE를 테스트하기 위해 구체화된 Uppaal 모델에서 생성됩니다. 본 연구는 오픈 소스 분산 애플리케이션의 신뢰성을 향상시키기 위한 형식적인 모델링, 검증 및 테스트 과정을 활용하는 이점을 강조합니다. 우리는 애플리케이션 모델링 및 추상 모델에서 구체적인 테스트를 생성하는 데 사용된 방법론을 논의하며, 식별되고 수정된 문제를 다룹니다.
다비드 바질레(목요일)는 이 질문을 연구했습니다.