본문 바로가기

전체 글

 (98)
CTL **CTL (Computation Tree Logic)**은 **분기 시계열 논리(branching-time temporal logic)**의 한 종류로, 시스템의 모든 가능한 미래 경로에 대해 명제를 기술하는 데 사용되는 형식 논리입니다. 주로 Model Checking에서 사용됩니다.---핵심 개념:CTL의 식은 항상 두 종류의 기호가 함께 쓰입니다:경로 한정자 (path quantifier):A: 모든 경로 (All paths)E: 어떤 경로 (Exists a path)시제 연산자 (temporal operator):X: 다음 (neXt)F: 미래에 언젠가 (Future)G: 항상 (Globally)U: ~까지 (Until)CTL에서는 항상 이 두 종류가 쌍으로 사용됩니다.예를 들어:AX p: 모든..
Model Checking **Model Checking(모델 검증)**이란, 형식적으로 명세된 시스템 모델이 요구사항을 만족하는지 자동으로 검증하는 기법입니다. 하드웨어, 소프트웨어, 통신 프로토콜, 임베디드 시스템 등에서 사용됩니다.---핵심 구성 요소:모델(Model): 시스템의 상태 전이 구조 (예: Kripke 구조)명세(Specification): 요구사항을 표현한 논리식 (보통 LTL, CTL 등)검증 엔진(Checker): 모델이 명세를 만족하는지 자동으로 판정---작동 방식:1. 시스템을 상태 전이 시스템으로 모델링(예: 어떤 상태에서 어떤 조건에 따라 다음 상태로 전이됨)2. 요구사항을 형식 논리로 기술(예: "항상 오류 상태에 빠지지 말 것" → AG ¬error)3. 검증 도구가 모든 가능한 실행 경로를 탐색..
TMP의 목적 컴파일 타임 코드 생성템플릿을 이용해 조건 분기, 반복, 계산 등을 컴파일 시점에 수행함으로써런타임 오버헤드를 줄이고타입에 따른 최적화된 코드를 자동 생성할 수 있게 하기 위해 도입·발전

티스토리툴바