선택한 단어 수는 입니다.
최소 단어 이상 선택하여야 합니다.
최소 단어 이상 선택하여야 합니다.
선택한 단어 수는 30입니다.
최대 10 단어까지만 선택 가능합니다.
최대 10 단어까지만 선택 가능합니다.
문제 정의
- 4장에서는 제안 내용을 시나리오를 대상으로 전체 과정을 설명한다. 그리고 명세가 변경되었을 때 개별 모델은 정확하지만 상호 작용에 문제를 발생될 수 있음을 시뮬레이터를 통해 확인하는 과정을 소개한다. 5장에서는 본 논문의 결론을 맺는다.
- 이 도구를 활용하여 사전에 모델 수준에서 상호 작용을 검사하고 시스템의 요구 사항을 위반하는지를 확인할 수 있다. 따라서 다양하게 변하는 환경에서 모듈 및 시스템의 품질을 보장할 수 있는 수단을 제공한다.
- 따라서 본 논문에서는 이러한 특징을 가지는 시스템의 품질 확보를 위한 다음과 같은 연구들을 소개한다.
- 이번 장에서는 사례 연구를 통해 다수의 시스템 구성 요소들이 상호 작용하면서 요구 사항을 부합하는 시나리오를 소개한다. 또한 시뮬레이터를 통해 요구 사항을 부합하지 못하는 경우를 확인하는 시나리오를 소개한다.
- 실현 가능하다는 것의 개념은 모델 검증[4]과 비교하여 설명할 수 있다. 모델 검증은 모델과 속성이 주어졌을 때 모델상에서 속성이 만족되는지를 확인하는 것이다. 만약 속성을 위반하는 하나의 경로(반례)를 발견하여 모델을 수정하였다 하더라도 탐색하지 않은 모델의 상태 공간이 존재하므로 모델이 완전히 속성을 만족하는 행위를 한다고 볼 수 없다.
- 본 논문에서 GR(1) 합성을 통해 생성된 모델들을 실행하기 위한 시뮬레이터를 개발하였다. 이 도구의 전체 모습은 Fig.
- 이번 장에서는 사례 연구를 통해 다수의 시스템 구성 요소들이 상호 작용하면서 요구 사항을 부합하는 시나리오를 소개한다. 또한 시뮬레이터를 통해 요구 사항을 부합하지 못하는 경우를 확인하는 시나리오를 소개한다.
- 이번 절에서는 앞서 소개한 아비터 시나리오에서 아비터의 명세가 변경되었을 때 전체 시스템의 행위가 요구 사항을 부합하지 않는 경우를 어떻게 발견하는지를 소개한다.
가설 설정
- 1) 로봇 H는 영역 {r1,...,r4}를 이동해야 한다.
- 2) 로봇 P는 영역 {r4,...,r5}를 이동해야 한다.
- 3) 영역 r4는 동시에 두 로봇이 위치할 수 없다.
- 5) 요청에 대한 승인을 받은 로봇만이 언젠가는 영역 r4를 지나갈 수 있다.
- 6) 요청에 대한 승인을 받은 로봇은 알람음을 발생한다.
- 변경되는 명세는 아비터이며 나머지 두 로봇의 명세는 변경되지 않는다고 가정한다. 그리고 형식화도 이전과 동일하다고 한다.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.