#model checking

상태 분석을 활용한 복잡한 임베디드 시스템에 대한 요구사항 생성하기

Motivation 시스템 엔지니어가 작성한 소프트웨어 요구사항과 소프트웨어 엔지니어가 작성한 코드상의 차이가 크다. 소프트웨어 엔지니어는 요구사항을 코드로 번역하여 시스템 엔지니어가 의도한 시스템의 행동에 부합하다는 기대를 해야만 한다. 해결 방법: State analysis방법을 사용하여 명시적으로 표현한다. Introduction State analysis방법론은 다음의 3가지 기본적 원칙을 주장(assert)한다. control은 system operation의 모든 측면을 포함한다. system under control의 모델을 통해 이해될 수 있음 system under control의 모델은 명시적으로 식별되고 시스템 엔지니어들 사이의 합의된 것들을 보장하는 방식이어야 함 소프트웨어 설계 및…