모델 체크의 원칙
Principles of Model Checking 전면 커버 | |
| 작가. | 크리스텔 바이어와 주스트 피에터 카토엔 |
|---|---|
| 주제 | 모델 체크 |
| 출판인 | MIT 프레스 |
발행일자 | 2008년 4월 25일 |
| 페이지 | 975 |
| ISBN | 9780262026499 |
모델 체크의 원칙은 모델이 사양 요건을 충족하는지 여부를 판단하는 문제를 자동화하는 컴퓨터 과학 분야인 모델 체크에 관한 교과서입니다.Christel Baier와 Joost-Pieter Katoen에 의해 쓰여졌고 2008년 MIT Press에 의해 출판되었다.
개요
도입부와 첫 번째 장에서는 모델 체크 분야의 개요를 설명합니다.기계 또는 프로세스의 모델을 분석하여 바람직한 특성이 유지되는지 확인할 수 있습니다.예를 들어, 자판기는 "잔액이 €0,00 이하로 떨어질 수 없다"는 특성을 충족할 수 있다.비디오 게임은 "플레이어의 생명이 0인 경우 게임은 패배로 끝난다"라는 규칙을 적용할 수 있습니다.자판기와 비디오 게임 모두 트랜지션 시스템으로 모델링할 수 있습니다.모델 체크는 그러한 요건을 수학 언어로 기술하고, 모델이 요건을 충족하고 있다는 증거를 자동화하거나, 모델에 결함이 있는 경우 반례를 발견하는 과정입니다.
두 번째 장에서는 알고리즘의 여러 부분(명령 세트)을 다른 기계 또는 기계의 부품에 의해 동시에 수행할 수 있는 동시 시스템에 대한 적절한 모델을 만드는 데 초점을 맞추고 있습니다.
제3장에서는 트랜지션 시스템이 충족할 수 있는 규칙 유형, 즉 선형 시간 속성을 살펴봅니다."어떤 교착 상태도 가능하지 않다"와 같은 안전 속성은 "불필요한 결과는 결코 발생할 수 없다"의 형태이다."공유 리소스는 결국 그것을 요구하는 컴포넌트에서 항상 사용할 수 있게 됩니다."와 같은 활성 속성은 "바람직한 결과는 결국 발생합니다."라는 형식입니다."신호등 색상 변경을 멈추지 않음"과 같은 공정성 특성은 전제조건으로 사용될 수 있다. 즉, 다른 속성을 추론할 수 있는 가정이다.
네 번째 장에서는 정규 및 정규 언어의 특성과 언어를 모델화하는 Büchi automata와 같은 이론적인 기계에 대해 설명합니다.특성 확인 또는 반례를 찾기 위한 모델 확인 알고리즘을 제공합니다.
다섯 번째 장과 여섯 번째 장에서는 특성을 표현하는 두 가지 공식 클래스인 선형 시간 논리(LTL)와 계산 트리 논리(CTL)를 살펴봅니다.LTL은 "모든 모노폴리 플레이어가 'Go'를 무한히 자주 통과한다"와 같이 시스템을 통과하는 경로에 대한 요구사항을 인코딩하고, CTL은 "어느 위치에서든 모든 플레이어가 결국 'Go'에 착지할 수 있다"와 같은 시스템 상태에 대한 요구사항을 인코딩한다.2개의 문법을 조합한 CTL* 공식도 정의되어 있습니다.이들 로직의 모델 체크 공식에 대한 알고리즘이 제공된다.
일곱 번째 장에서는 이중 시뮬레이션과 같은 전이 시스템을 비교하는 공식 방법을 살펴봅니다. 여덟 번째 장에서는 모델의 특성을 검증하는 데 필요한 계산을 줄이는 것을 목표로 하는 부분 순서 감소에 대해 살펴봅니다.9장과 10장은 클럭 속도(시간 자동 장치) 또는 확률(마르코프 체인에 기초한 확률 자동 장치)의 추가를 포함하여 이전에 고려된 로직과 자동 장치에 대한 확장에 관한 것이다.
접수처
컴퓨터 저널에 기고한 프랑수아 라루시니는 이 책을 "인상적"이라며 연구원, 강사, 학생, 엔지니어들에게 추천했다.Larussinie는 교과서가 포괄적이고 접근하기 쉽게 쓰여져 있으며, 많은 사례와 연습, 그리고 주요 개념에 대한 동기 부여 아이디어를 가지고 있다는 것을 발견했습니다."통합 프레임워크"를 사용하여 처음 7장은 고전 이론을 다루고 마지막 3장은 모델 확인의 [1]확장을 다룬다.
ACM Computing Reviews에서 Gabriel Ciobanu는 이 교과서가 고급 학부 과정 또는 대학원 과정에서도 사용될 수 있으며 연구원들에게도 유용할 것이라고 생각했습니다.Ciobanu는 "명료하고 직관적인" 프레젠테이션을 높이 평가하면서 "기본 개념, 깊은 이론적 결과 및 모델 체크 연구의 고급 주제를 다루는 교육학적 접근 방식을 높이 평가해야 한다"[2]고 말했습니다.
2014년에, 이 책은 [3]BKCI가 모니터링한 가장 많이 인용된 5개의 학술 교재 중 하나였다.
레퍼런스
- ^ Laroussinie, François (2010). "Principles of Model Checking (Review)". The Computer Journal. 53 (5): 615–616. doi:10.1093/comjnl/bxp025.
- ^ Ciobanu, Gabriel (8 January 2009). "Principles of Model Checking (Review)". ACM Computing Reviews.
- ^ Kousha, Kayvan; Thelwall, Mike (1 March 2016). "Can Amazon.com Reviews Help to Assess the Wider Impacts of Books?". Journal of the Association for Information Science and Technology: 580.
추가 정보
- Lange, Martin (2010), MathSciNet, MR 2493187
{{citation}}: CS1 유지보수 : 제목 없는 정기 (링크)
