Event-B 모델 개발

Event-B 모델은 이산 전이 시스템입니다. CONTEXT는 고정 집합, 상수, 공리를 담고, MACHINE은 변수, 불변식, 보호된 이벤트를 담습니다. 이 스킬은 ProB로 도달 가능한 동작을 검사하고 well-definedness를 게이트합니다. 대화형 Rodin 증명을 작성하지 않습니다.

1. 필요한 도구 확인

rossi 0.1.8+ 및 eventb-animate 6.4+가 필요합니다. 확인하십시오. 직접 설치하거나 업그레이드하지 마십시오. 둘 중 하나가 없거나 구버전이면 중단하고 사용자에게 요청하십시오.

command -v rossi eventb-animate
rossi --version
eventb-animate --version

2. 모델링 전 범위 정의

모델의 README.md에 간단한 요구사항 시트를 작성하십시오.

시스템 경계와 명시적 제외사항;
관찰 가능한 이벤트와 수행 주체;
상태 유형과 항상 유지되어야 하는 안전 속성;
하나의 도달 가능한 성공 시나리오, 하나의 중요한 금지 시나리오, 종료 상태가 의도적인지 여부.

상당한 규모의 모델이나 다단계 정제가 있는 경우, 각 레벨마다 한 행씩 요구사항-정제 대장을 추가하십시오: 요구사항/표준 절, 새롭거나 대체된 상태, 영향받는 이벤트, 불변식/접합 관계, 검증 질문. 행에 관련 없는 우려사항이 섞여 있으면 레벨을 분할하십시오.

기본적으로 하나의 머신을 사용하고, 고정 데이터는 독립적인 우려사항 수만큼 여러 개의 작은 컨텍스트로 분할하십시오. 정제 레벨은 별개의 요구사항을 분리하거나 데이터 표현을 대체할 때만 추가하고, 그 이유와 접합 불변식을 먼저 작성하십시오. 정제는 도구이지 필수 의식이 아닙니다.

각 모델은 자체 프로젝트 디렉토리에 두십시오. 구성 요소당 하나의 파일을 사용하고, 파일 이름은 구성 요소 이름을 따르십시오. .eventb 파일에 산문 주석을 넣지 말고 설명은 README.md에 유지하십시오.

3. 관련 참조만 읽기

필요	읽을 것
정확한 `.eventb` 문법 및 동작 형식	`references/syntax.md`
연산자 또는 우선순위	`references/math-toolkit.md`
상태, 불변식 또는 이벤트 선택 도움	`references/modelling.md`
실제 정제 단계 또는 체인 계획	`references/refinement.md`
핵심 반응형 시스템 패턴	`references/patterns.md`의 해당 제목
이산 시간, 마감, 모드 또는 센서/액추에이터	`references/patterns-control.md`
다중 참여자: 토폴로지, 라운드, 합의, 채널, 장기 실행 작업	`references/patterns-distributed.md`
접근 제어, 인가 정책 또는 예약	`references/patterns-security.md`
사후조건에서 루프 도출 또는 인터프리터/ISA	`references/patterns-algorithms.md`
CLI 문제 해결 또는 조건부 고급 명령	`references/tooling.md`
최종 설계 검토	`references/best-practices.md`

증인 또는 데이터 정제가 포함된 경우에만 examples/counter/에서 시작하고, 이벤트 분할/수렴에는 examples/cars_on_bridge/를, 종료 알고리즘에는 examples/array_maximum/를 사용하십시오. 작은 단일 머신 모델을 시작하기 위해 예제를 읽지 마십시오.

4. 가장 작은 유용한 모델 작성

캐리어 집합과 고정 정책/구성은 컨텍스트에 넣으십시오.
첫 번째 불변식으로 모든 변수에 타입을 지정한 다음 실제 안전 규칙을 명시하십시오.
감지 또는 제어가 시스템 경계를 넘을 때 물리적, 보고된, 명령된 상태를 구분하고 허용된 지연/불확실성을 명시하십시오.
INITIALISATION이 모든 불변식을 확립하도록 하십시오.
각 이벤트에 기능적 및 전이 전용 요구사항과 불변식 보존에 필요한 모든 가드를 제공하십시오. 동작은 동시에 실행되며 할당되지 않은 변수는 변경되지 않은 상태로 유지됩니다.
나중 상태 목표가 관찰해야 할 중요한 결과를 상태로 표현하십시오. 단지 커버리지를 얻기 위해 no-op 이벤트를 추가하지 마십시오. 활성화된 no-op은 데드락 및 라이브니스 동작을 변경합니다.
유한 검사 시나리오는 작게 유지하십시오. 광범위한 비결정적 매개변수는 연산 활성화를 배가시키고 유한 검사를 불완전하거나 느리게 만들 수 있습니다.

5. 핵심 게이트 실행

관련 없는 모델이 포함된 상위 디렉토리가 아닌 모델의 프로젝트 디렉토리에서 실행하십시오. .zip을 빌드하십시오. 애니메이터가 필요한 검사된 파일이 포함됩니다.

rossi fmt -i .
rossi validate .
rossi fmt --check .
rossi build . -o /tmp/model.zip
eventb-animate --json /tmp/model-report.json /tmp/model.zip
eventb-animate wd /tmp/model.zip

다음 조건에서만 결과를 수락하십시오.

validation 및 build에 오류가 없습니다. missing or ill-typed witness 및 event is inaccurate 경고는 명령이 0으로 종료되더라도 실패로 간주합니다.
보고서에 status: "ok"가 있고 불변식 위반이 없습니다.
예상치 못한 데드락이 없습니다. 의도적인 종료 상태의 경우 종료 술어를 문서화하고 데드락 자유를 주장하는 대신 --no-deadlock으로 다시 실행하십시오.
사람이 읽는 Covered operations 블록에 예상 이벤트가 포함되어 있습니다(보고서 v3는 연산 커버리지를 저장하지 않으므로 감사가 필요할 때 명령 출력을 캡처하십시오).
completion.classification이 유한 수락 시나리오에 대해 complete입니다.
모든 well-definedness 의무가 해소되었습니다.

종료 코드 0은 완전성의 증거가 아닙니다. 유한 모델이 불완전하다고 보고되면 이유와 관련 ProB 한계를 검사하십시오.

eventb-animate info --prefs /tmp/model.zip \
  | rg 'MAX_(INITIALISATIONS|OPERATIONS)|DEFAULT_SETSIZE'

알려진 유한 선택을 열거할 수 있을 만큼만 MAX_INITIALISATIONS 또는 MAX_OPERATIONS를 높인 후 다시 실행하고 completion.classification: "complete"를 요구하십시오. 의도적으로 일반/무제한 모델의 경우 경계 결과를 정직하게 보고하고 철저한 게이트가 중요할 때 별도의 작은 유한 시나리오를 추가하십시오.

정제 체인이 있는 경우 모든 레벨에 대해 -m <machine>으로 모델 검사와 wd를 반복하십시오.

6. 질문에 답할 때 표적 증거 추가

상태 술어에 도달할 수 있는지에 대한 질문일 때 목표 추적을 사용하십시오.

eventb-animate -m M --goal '<predicate>' --no-invariant --no-deadlock \
  --save /tmp/scenario.json /tmp/model.zip
eventb-animate replay -m M -t /tmp/scenario.json /tmp/model.zip

목표에 도달하면 의도적으로 종료 코드 1을 반환합니다. PERFECT 재생을 요구하십시오. 불변식 또는 데드락 실패 시 모델을 변경하기 전에 해당 반례를 저장하고 재생하십시오.

상태 목표는 동작이 없거나 가드만 있는 이벤트가 발생했음을 증명할 수 없습니다. 활성화 상태에 도달하는 즉시 중지될 수 있습니다. 완전 검사의 Covered operations 블록을 통해 특정 전환을 확인하거나 테스트 생성으로 목표를 설정하십시오.

eventb-animate testgen -m M --operations EVENT_NAME \
  --out /tmp/scenario-traces /tmp/model.zip

더 좁은 목적이 적용될 때만 다음을 사용하십시오.

testgen: 특정 전환을 입증하거나 재생 가능한 연산 픽스처를 생성합니다. 철저한 검사보다 강력한 게이트가 아니며 "uncovered"는 결정적이지 않습니다.
--symbolic ic3|kinduction: 무제한 불변식 안전성; 데드락, 이벤트 커버리지를 확인하지 않으며 추적을 제공하지 않습니다.
po: 이미 .bpo/.bps 증명을 보유한 기존 Rodin 프로젝트를 게이트합니다.
import/export: Rodin 상호 교환을 위한 것으로 일반 작성 루프가 아닙니다.

이러한 조건부 워크플로는 references/tooling.md를 참조하십시오. 기본 ProB 백엔드가 일반 작성 경로입니다.

7. 읽기 쉬운 산출물로 마무리

.eventb 파일과 범위, 모델 형태, 일반 언어로 된 안전 불변식, 정제 대장(있는 경우), 정확한 검사 명령, 완전성, 이벤트 커버리지, WD 결과 및 의도적인 추상화를 포함한 짧은 README.md를 제공하십시오. 깨끗한 경계 실행은 "경계 내에서 버그를 찾지 못함"을 의미합니다. 완전한 유한 실행은 검사된 도달 가능한 동작만 증명합니다. 위반 상태가 도달 불가능하기 때문에 너무 강하고 비귀납적인 불변식을 여전히 수락할 수 있습니다. Event-B 불변식/정제 증명 의무를 해소하지 않습니다. 해당 주장을 뒷받침하는 것은 적용 가능한 증명 게이트뿐입니다. references/refinement.md, "모델 검사는 증명이 아님"을 참조하십시오.

Event-B 모델 개발 스킬