 모바일 환경을 위한 UBIFS 안정성 검증
삼성전자 - 정형기법을 활용한 UBIFS 안정성 검증 (2009.9.1 ~ 2009.12.31 ) 1. 과제개요 가. UBIFS를 적용한 파일 시스템의 적용 및 안정성 검증 ▣ 핸드폰, MP3, PMP 등 개인 휴대장치로부터 자동차, 항공, 철도 제어 시스템, 크게는 원자력발전소 제어 시스템에 이르기까지 수없이 많은 임베디드 시스템이 사회전반에 퍼져있으며 임베디드 시스템의 수는 앞으로도 기하급수적으로 증가할 추세를 보임. 플래시메모리는 상대적으로 높은 안정성과 고용량을 저장할 수 있다는 장점으로 인해, 임베디드 시스템의 대표적인 저장장치로 자리매김 하고 있음.
▣ UBIFS의 경우 매우 최신의 파일시스템이라 그 안정성적인 측면은 검증되지 않았기 때문에, 이를 보다 체계적으로 검증하고, 또한 UBIFS의 숨은 오류들을 검증하기 위해 본 과제에서는 소스코드 기반의 모델체킹 기법을 적용하고, 이를 통해 UBIFS 뿐만 아니라 오픈소스를 포함한 다른 기존의 소스 코드를 검증할 수 있는 기반을 마련할 수 있을 것이라고 예상됨.
나. 플래쉬 메모리를 위한 파일시스템의 발전 ▣ 시대의 흐름에 맞추어 JFFS, JFFS2, YAFFS 등이 플래시 메모리 저장장치의 파일시스템으로 개발되어왔지만, 상기 언급된 파일시스템은 각기 낮은 성능과 제약사항을 가지고 있어 전체적인 플래시 저장장치의 성능저하를 가져옴. 이들 파일 시스템은 모두 메모리 구조를 위한 메모리 사용량이 크고, 마운트 시 모든 블럭을 스캔해야 하므로 마운트 시간이 느린 문제가 있으며, 쓰기 성능이 상대적으로 느림. 이러한 플래시 파일시스템의 성능적 제약을 해소하기 위해 최근에 UBIFS가 개발됨.
▣ UBIFS는 JFFS2 파일 시스템이 가지고 있는 장점인 동적 압축, 전원 차단에 대한 내성 및 복구 가능성 등을 유지함과 동시에 마운트 성능 개선, 대용량 파일 처리 성능 개선, 쓰기 성능 개선 등을 목표로 하여 오픈 소스로 개발되었고, 008년 10월 리눅스 커널 2.6.27 이후로 현재 리눅스 운영체체에 탑재 됨.
▣ UBIFS는 JFFS2의 쓰기성능을 대폭 향상시켰지만, 상용 임베디드 시스템에 탑재되기 위해서는 안정성검증이 필수적 이지만, UBIFS는 가장 최신의 파일시스템이기 때문에 아직 충분한 안정성검증이 이루어 지지 않은 상태.
다. 소스 기반의 모델체킹 기법을 적용하여 UBIFS의 안정성 검증을 목표 ▣ 본 연구에서는 UBIFS의 sudden power off 등의 이벤트에 대한 안정성을 보다 체계적으로 검증하고, 또한 UBIFS의 숨은 오류들을 검증하기 위해 본 과제에서는 소스코드 기반의 모델체킹 기법을 적용할 것임. 정형 기법의 일종인 모델 체킹 기법은 검증하고자 하는 시스템에 대한 모델과 그 시스템이 만족해야 할 속성을 정형적으로 명세한 후, 자동화된 도구를 이용하여 시스템이 가질 수 있는 모든 상태공간을 탐색하여 시스템이 그 속성을 만족하는지를 검사하는 기법임.
▣ 그래프 알고리즘, 자료 구조, 논리학을 근간으로 한 수학적 모델과 이론을 기반으로 하는 모델 체킹은 시스템이 가질 수 있는 일부의 상태만을 확인하는 테스팅이나 시뮬레이션과 달리, 시스템의 가질 수 있는 모든 상태에 대하여 시스템에 요구되는 속성이 만족하는지를 확인 함.
▣ 현재까지 제안된 대부분의 자동화된 검증도구는 UBIFS와 같은 시스템 소프트웨어를 검증하기에는 어려움이 존재하기 때문에, 검증대상과 아닌 것을 잘 경계지어 검증대상이 아닌 코드는 스터브(Stub)로 만들고, 검증대상 자체를 구동시키기 위한 하니스(Harness)를 통하여 파일시스템이 응용프로그램의 요청 없이도 수행 될 수 있도록 환경을 구성하여 검증 하고, 이를 통해 UBIFS 뿐만 아니라 오픈소스를 포함한 다른 기존의 소스 코드를 검증할 수 있는 기반을 마련할 수 있을 것이라고 예상됨. 2. 추진배경 가. 플래시 메모리를 위한 새로운 파일 시스템의 출현 : UBIFS ▣ 다양한 분야에 사용되고 있는 플래시 메모리
- 반도체를 이용한 드라이브는 임베디드 시스템 분야를 비롯하여 범용 컴퓨터에까지 그 적용 영역이 넓혀지고 있으며 이를 위한 다양한 파일 시스템이 개발 및 제안됨.
- NOR 및 NAND형을 비롯하여 다양한 형태로 발전되고 있는 flash memory는 비휘발성 메모리로서 전원 유무에 관계없이 데이터를 유지할 수 있으나, 데이터를 삭제 가능한 횟수가 정해져 있다는 단점이 있음.
- 플래시 메모리의 수명 및 효율적인 동작을 보장하기 위해 wear-leveling, garbage collection 등과 같은 다양한 기법들이 요구되며, 이러한 기법들은 플래시기반 파일 시스템의 핵심 기술.
▣ 기존 플래시 메모리 기반 파일 시스템의 한계
- 기존에 제안된 대표적인 플래시 메모리 기반 파일 시스템 : JFFS, JFFS2, YAFFS 등.
- NOR 플래시 메모리를 위해 설계된 JFFS는 garbage collection을 통해 각 메모리 블록의 데이터 삭제 횟수를 균등하게 유지하고, 가용 메모리 용량을 효율적으로 관리. 그러나 garbage collection으로 인한 빈번한 데이터 삭제는 오히려 플래시 메모리의 수명을 단축시킴.
- NAND 플래시 메모리를 위한 JFFS2는 JFFS의 문제점을 개선하기 위해 새로운 garbage collection 알고리즘을 제안하였으나, 데이터 삭제 횟수를 균등하게 관리하기 위해 각 블록의 데이터를 이동하는 과정에서 여전히 많은 횟수의 삭제 동작을 수행.
- YAFFS는 JFFS2와 같이 NAND 플래시 메모리를 위한 것으로, 각 블록에 연속적인 숫자를 할당함으로써 파일 시스템의 마운트 후 램(RAM)으로 복구하는 과정이 기존의 파일 시스템에 비해 빠름. 그러나 YAFFS는 기존의 파일 시스템에 비해 메모리 쓰기 과정에서 제약이 커짐.
▣ UBIFS: UBI file system
- 기존의 플래시 메모리 파일 시스템과 달리 특정 플래시 메모리의 종류에 제한 받지 않는 UBIFS가 Nokia에 의해 개발됨. UBIFS는 다양한 플래시 메모리에 접근하기 위한 API를 제공하는 Memory Technology Devices(MTD)를 통해 플래시 메모리를 추상화 함으로써 파일 시스템과 플래시 메모리간의 의존성을 제거함. 또한, Unsorted Block Images(UBI)를 기반으로 함으로써 wear-leveling, 불량 블록 관리, 동적 볼륨 관리 등이 가능.
<그림 1 UBIFS를 사용한 플래시 메모리 파일 시스템의 레이어 계층도> - 특히, UBIFS는 JFFS2 파일 시스템이 가지고 있는 장점인 동적 압축, 전원 차단에 대한 내성 및 복구 가능성 등을 유지함과 동시에 마운트 성능 개선, 대용량 파일 처리 성능 개선, 쓰기 성능 개선 등을 목표로 하여 오픈 소스로 개발됨.
- 이러한 UBIFS는 기존의 파일 시스템에 비해 뛰어난 확장성 및 성능을 가지고 있으며, 이로 인해 향후 모바일 멀티미디어 시스템과 같이 고성능 시스템에서 기존의 시스템에 비해 뛰어난 성능을 보일 것으로 예상됨.
- 2008년 10월 리눅스 커널 2.6.27버젼에 처음으로 릴리즈 되었으나, UBIFS를 기반으로 상용화된 제품은 현재까지 전무한 상태임. 이는 현재까지UBIFS의 안정성에 대한 검증이 충분히 이루어지지 않았기 때문으로 상용화 시도 이전에 UBIFS에 대한 안정성 검증이 필수적임.
나. 정형 기법을 이용한 UBIFS의 안정성 검증 ▣ 정형 기법 소개
- 정형기법은 수학적 기반으로 엄격하게 정의된 언어를 통해 시스템의 명세와 설계를 수행하고, 수학적 증명을 통해 검증함으로써 모호한 자연어 명세와 일반적 검증 절차에서 발생할 수 있는 인적 오류의 개연성을 억제함.
- 일반적인 개발 방법론 상에서 설계 혹은 시스템의 모든 관련 요소들에 대한 완벽한 검증을 수행한다는 것은 사실상 불가능. 안전성과 신뢰도가 중요한 시스템일수록 정형기법을 적용함으로써 개발 비용 및 일정을 현격히 감소시키고 동시에 설계의 완전성을 보장함.
- 안정성과 신뢰성이 요구되는 시스템의 개발에 있어 요구분석, 명세, 설계, 그리고 검증과 시험은 일반적인 절차 통제만으로 완벽한 결과를 보장할 수 없음. 하지만 시스템의 무결성과 안전성을 추구하는 정형기법은 완벽한 설계와 신뢰할만한 구현물을 보장함.
- 보안, 원자력, 항공, 우주 및 자동차 산업 등에서 필요한 디지털 제어 시스템이나 유비쿼터스 컴퓨팅의 기반이 되는 임베디드 시스템 등의 다양한 분야에 적.
▣ 모델 체킹 기법
- 정형 기법의 일종. 검증하고자 하는 시스템에 대한 모델과 그 시스템이 만족해야 할 속성을 정형적으로 명세한 후, 자동화된 도구를 이용하여 시스템이 가질 수 있는 모든 상태공간을 탐색하여 시스템이 그 속성을 만족하는지를 검사하는 기법. 특히 속성이 만족하지 않을 때에는 그 반례를 자동으로 생성하여 시스템의 수정이 용이하게 함.
<그림 2 모델 체킹 기법의 개요도> - 시스템이 가질 수 있는 일부의 상태만을 확인하는 테스팅이나 시뮬레이션과 달리, 시스템의 가질 수 있는 모든 상태에 대하여 시스템에 요구되는 속성이 만족하는지를 확인하므로 안전 필수 시스템의 검증에 필수적으로 요구됨.
- 모델 체킹 기법은 그래프 알고리즘, 자료 구조, 논리학을 근간으로 한 수학적 모델과 이론을 기반으로 함. 그러나 자동화된 도구들로 인하여 모델 체킹을을 위한 많은 전문 지식을 요구하지 않는 “push-button” 기법에 가까우므로 산업 현장에의 도입이 쉬움. 현재 Lucent, IBM, Intel, Fujitsu, Siemens, Motorola 등의 기업에서 하드웨어 검증에 모델 체킹 기법을 사용함.
- 최근에는 시스템의 구현된 코드에서 자동/반자동으로 모델을 추출하는 다양한 기법들이 연구되고 있음. C 코드의 경우 마이크로소프트사의 SLAM 프로젝트, 버클리 대학의 BLAST, 카네기 멜론 대학의 CBMC와 SATAbs 등이 있음.
- 고신뢰 소프트웨어 개발을 위한 확인 및 검증 기법으로 국내에서는, 타겟 정형 명세 및 프로그램을 기존에 국외에서 개발되어 사용되고 있는 모델 체킹 도구나 테스팅 도구들의 입력으로 자동 변환한 후 기존의 도구들을 활용하여 확인 및 검증을 수행한 사례가 많음.
|
