개요Event-B는 정형 기법(Formal Method)을 활용한 시스템 모델링 및 검증 프레임워크로, 복잡한 시스템의 정확성과 일관성을 수학적으로 보장할 수 있도록 설계된 언어 및 개발 방법론입니다. 주로 임베디드 시스템, 안전 필수 시스템, 프로토콜 설계 등 고신뢰성이 요구되는 분야에서 활용되며, 추상화(abstraction)와 정제(refinement)를 핵심 개발 흐름으로 사용합니다.1. 개념 및 정의Event-B는 Jean-Raymond Abrial이 개발한 정형 기법 언어로, **상태 기반 모델링(State-Based Modeling)**을 통해 시스템 동작을 정의합니다.B-Method의 확장: Event 중심의 상태 전이 모델링정형 명세(Formal Specification) + 수학적 증명..
