추상모델체크

컴퓨터 과학 및 수학에서 추상화 모델 확인은 모델을 단독으로 개발하는 데 실제 표현이 너무 복잡한 시스템을 대상으로 합니다.따라서 이 설계는 축소된 "추상" 버전으로 번역됩니다.

변수 집합은 값의 변화에 따라 볼 수 있는 변수와 보이지 않는 변수로 구분됩니다.실제 상태 공간은 보이는 공간 중 더 작은 집합으로 요약됩니다.

갈루아 접속

실제와 추상 상태 공간은 갈로아가 연결되어 있습니다.즉, 추상적인 공간에서 요소를 추출하여 구체화하고 구체화한 버전을 추상화하면 그 결과는 원본과 같아진다는 것을 의미합니다.한편, 실제의 공간으로부터 요소를 선택해 추상화해, 추상화하면, 최종적인 결과는 오리지날의 슈퍼 세트가 됩니다.

그것은,

$displaystyle$ \eta$$$（$$$$}$ \ $displaystyle$ \theta$）$ $=$ abstract
${\$ {$display style$ \theta$$} ( $)$ { $displaystyle$ \eta$$} ( $real$ )$${\ {\ \ displaystyle \ $supseteq$} ${\displaystyle \mathrm{real}}$$$

「 」를 참조해 주세요.

레퍼런스

• Edmund M. Clarke and Orna Grumberg and David E. Long (1994). "Model checking and abstraction". ACM Transactions on Programming Languages and Systems. 16 (5): 1512–1542. CiteSeerX 10.1.1.79.3022. doi:10.1145/186025.186051.

이 문서에는 추가 카테고리 또는 보다 구체적인 카테고리가 필요합니다. 유사한 기사와 함께 게재할 수 있도록 카테고리를 추가해 주십시오.(2021년 12월)