머리말
오늘날 소프트웨어는 우리 사회의 기반 시설 곳곳에 깊숙이 자리 잡고 있습니다. 항공기 제어 시스템부터 의료 기기, 원자력 발전소, 자율 주행 자동차, 금융 시스템에 이르기까지, 소프트웨어의 오작동은 막대한 재산 피해는 물론 인명 손실까지 초래할 수 있습니다. 이처럼 ‘고신뢰성(High-Integrity)’이 필수적인 분야에서는 단순히 기능 구현을 넘어, 소프트웨어가 의도한 대로 정확하고 안전하게 동작한다는 것을 보장하는 것이 무엇보다 중요합니다.
이러한 배경 속에서 소프트웨어의 정확성과 안전성을 수학적 원리에 기반하여 증명하려는 노력, 즉 ‘정형 검증(Formal Verification)’ 기법이 주목받고 있습니다. 그리고 그 노력의 중심에 있는 강력한 도구 중 하나가 바로 SPARK 프로그래밍 언어입니다. SPARK는 강력하고 안전한 프로그래밍 언어로 정평난 Ada를 기반으로 하면서, 정형 검증 기법을 언어 자체에 통합하여 설계 단계부터 코드의 논리적 결함을 체계적으로 제거하고, 특정 종류의 런타임 오류가 절대로 발생하지 않음(Absence of Runtime Errors, AoRTE)을 증명할 수 있도록 특별히 설계되었습니다. SPARK를 사용하면 개발 초기 단계에서부터 버그를 효과적으로 찾아내고 수정하여, 테스트만으로는 달성하기 어려운 수준의 소프트웨어 품질과 신뢰성을 확보할 수 있습니다.
이 책 『SPARK 프로그래밍』은 SPARK 언어의 강력함을 활용하여 견고하고 신뢰할 수 있는 소프트웨어를 개발하고자 하는 모든 분들을 위한 안내서입니다. 프로그래밍 경험이 적은 초급자부터, 실무에서 정형 기법 도입을 고려하는 중급 개발자, 그리고 복잡한 시스템의 안전성 증명에 도전하는 고급 사용자까지, 각자의 수준에 맞춰 SPARK의 핵심 개념부터 고급 활용 기법까지 체계적으로 학습할 수 있도록 구성했습니다.
1부: SPARK 시작하기에서는 SPARK가 무엇이며 왜 필요한지, Ada 언어와의 관계는 어떠한지를 명확히 설명하고, SPARK 개발 환경 설정부터 기본적인 문법과 핵심 기능인 ‘계약(Contract)’ 기반 설계의 기초를 다룹니다. 초급자도 쉽게 따라 하며 SPARK 프로그래밍의 첫걸음을 뗄 수 있도록 예제를 통해 설명합니다.
2부: 실용적인 SPARK 프로그래밍과 검증에서는 다양한 종류의 계약(사전/사후 조건, 타입/루프 불변식 등)을 심도 있게 다루고, SPARK의 핵심 검증 도구인 GNATprove를 활용한 정적 분석 및 증명 워크플로우를 상세히 배웁니다. 모듈화된 소프트웨어 설계 방법과 실제 코드 검증 과정에서 마주칠 수 있는 문제들을 해결하는 실용적인 기법, 그리고 일반적인 SPARK 프로그래밍 패턴을 익혀 중급 개발자로 성장할 수 있도록 돕습니다.
3부: 고급 주제 및 응용에서는 실시간 및 동시성 시스템 개발을 위한 Ravenscar 프로파일, 자동 증명 도구의 한계를 넘어서는 고급 증명 기법, 하드웨어 제어를 위한 저수준 프로그래밍 방법, 그리고 실제 산업 분야에서의 SPARK 적용 사례 연구를 통해 고급 사용자들이 SPARK의 잠재력을 최대한 활용할 수 있는 지식과 기술을 제공합니다.
이 책을 효과적으로 학습하기 위해 기본적인 프로그래밍 개념(변수, 제어문, 함수 등)에 대한 이해가 있으면 좋습니다. Ada 언어에 대한 사전 지식이 있다면 SPARK를 배우는 데 도움이 되겠지만, 필수적인 것은 아닙니다. SPARK의 핵심적인 부분과 Ada와의 차이점은 책 전반에 걸쳐 충분히 설명됩니다.
SPARK를 배우는 여정은 때로는 코드의 모든 측면을 명시적으로 증명해야 하기에 도전적일 수 있습니다. 하지만 그 과정을 통해 얻게 되는 소프트웨어의 품질과 신뢰성에 대한 깊은 이해와 확신은 무엇과도 바꿀 수 없는 귀중한 자산이 될 것입니다. 이 책이 여러분의 SPARK 학습 여정에 든든한 동반자가 되어, 궁극적으로는 우리 사회를 더욱 안전하고 신뢰할 수 있는 곳으로 만드는 데 기여할 수 있기를 진심으로 바랍니다.
목차
1부: SPARK 시작하기 (초급자)
- 1. SPARK 소개
- 2. SPARK 언어 기초
- 2.1 기본 문법 구조
- 2.1.1 프로그램 단위 (패키지, 서브프로그램)
- 2.1.2 선언과 문장
- 2.1.3 주석과 가독성
- 2.2 데이터 타입
- 2.2.1 스칼라 타입 (정수, 열거형, 부동소수점 – 제약 사항 포함)
- 2.2.2 배열 타입
- 2.2.3 레코드 타입
- 2.2.4 타입 선언과 서브타입
- 2.3 제어 흐름
- 2.3.1 조건문 (if, case)
- 2.3.2 반복문 (loop, while, for) – 종료 증명 관련 소개
- 2.3.3 예외 처리 (SPARK에서의 제한적 사용)
- 2.4 서브프로그램
- 2.4.1 프로시저와 함수 정의
- 2.4.2 파라미터 모드 (in, out, in out)
- 2.4.3 기본적인 서브프로그램 예제
- 3. 계약(Contract) 기반 설계 입문
- 3.1 계약이란 무엇인가?
- 3.1.1 Design by Contract 개념
- 3.1.2 SPARK에서 계약의 역할
- 3.2 사전조건(Precondition)과 사후조건(Postcondition)
- 3.2.1 Pre 키워드 사용법
- 3.2.2 Post 키워드 사용법
- 3.2.3 Old 속성 소개
- 3.3 간단한 계약 작성 연습
- 3.3.1 기본적인 함수/프로시저에 계약 추가하기
- 3.3.2 계약 위반 시 발생하는 일
- 3.4 정적 분석 소개
- 3.4.1 컴파일 타임 검증의 개념
- 3.4.2 계약이 정적 분석을 돕는 방법
2부: 실용적인 SPARK 프로그래밍과 검증 (중급자)
- 4. SPARK 계약 심화
- 4.1 타입 불변식(Type Invariant)
- 4.1.1 Type_Invariant 정의 및 활용
- 4.1.2 프라이빗 타입과 불변식
- 4.2 서브프로그램 계약 심화
- 4.2.1 계약 내 표현식과 함수 사용
- 4.2.2 Depends 계약 (의존성 명시)
- 4.2.3 Global 계약 (전역 변수 접근 명시)
- 4.3 루프 불변식(Loop Invariant)
- 4.3.1 루프 종료 증명 (Loop_Variant)
- 4.3.2 루프 속성 증명 (Loop_Invariant)
- 4.3.3 루프 불변식 작성 기법
- 4.4 단언(Assertion)과 검사(Check)
- 4.4.1 Assert 프라그마
- 4.4.2 Check 프라그마 (런타임 검사 제어)
- 4.4.3 증명 보조 도구로서의 단언
- 4.1 타입 불변식(Type Invariant)
- 5. SPARK 검증 워크플로우
- 5.1 흐름 분석(Flow Analysis)
- 5.1.1 데이터 흐름 분석 (초기화, 사용되지 않는 변수 등)
- 5.1.2 정보 흐름 분석 (보안 속성 검증)
- 5.2 증명 의무(Proof Obligation) 생성
- 5.2.1 계약으로부터 증명 의무 생성 과정
- 5.2.2 다양한 종류의 증명 의무 (런타임 에러 방지, 계약 만족 등)
- 5.3 GNATprove 도구 활용
- 5.3.1 GNATprove 실행 및 옵션 설정
- 5.3.2 분석 결과 해석 (증명 성공, 실패, 타임아웃)
- 5.3.3 증명 실패 원인 분석 및 디버깅
- 5.4 증명 불가능한 코드 처리
- 5.4.1 정당화(Justification) 사용
- 5.4.2 외부 가정(Assumption) 도입
- 5.4.3 코드 재설계 고려
- 5.1 흐름 분석(Flow Analysis)
- 6. 모듈성과 데이터 추상화
- 6.1 패키지(Package) 설계
- 6.1.1 명세부(Specification)와 구현부(Body) 분리
- 6.1.2 정보 은닉 (Private/Limited Private 타입)
- 6.1.3 패키지 수준 계약 (Package_Invariant)
- 6.2 추상 데이터 타입(ADT) 구현
- 6.2.1 Private 타입을 이용한 ADT
- 6.2.2 Limited Private 타입을 이용한 ADT (복사, 할당 제어)
- 6.2.3 ADT와 계약의 결합
- 6.3 유령 코드(Ghost Code) 활용
- 6.3.1 유령 변수, 함수, 타입 소개
- 6.3.2 증명을 위한 추상 모델 구축
- 6.3.3 유령 코드 작성 주의사항
- 6.4 라이브러리 단위와 의존성 관리
- 6.4.1 with 및 use 절
- 6.4.2 프로젝트 파일(.gpr)을 이용한 빌드 관리
- 6.1 패키지(Package) 설계
- 7. 일반적인 SPARK 패턴 및 관용구
- 7.1 상태 기계(State Machine) 구현 및 검증
- 7.2 안전한 자원 관리 (메모리, 파일 등)
- 7.3 배열 및 인덱스 안전성 보장 기법
- 7.4 계약을 이용한 방어적 프로그래밍
- 7.5 수학적 모델과의 연계 (정수, 부동소수점 연산 검증)
3부: 고급 주제 및 응용 (고급자)
- 8. 동시성 및 실시간 시스템
- 8.1 Ravenscar 프로파일 소개
- 8.1.1 실시간 시스템을 위한 Ada/SPARK 제한 사항
- 8.1.2 태스크(Task)와 보호 객체(Protected Object) 기본
- 8.2 보호 객체를 이용한 안전한 공유 데이터 접근
- 8.2.1 보호 프로시저, 함수, 엔트리
- 8.2.2 보호 객체 계약 (Protected_Invariant)
- 8.3 태스킹 계약 및 분석
- 8.3.1 태스크 수준 계약 (Task_Invariant)
- 8.3.2 교착 상태(Deadlock) 및 경쟁 상태(Race Condition) 방지 분석
- 8.4 타이밍 분석 고려 사항
- 8.4.1 WCET(Worst-Case Execution Time) 분석 연계
- 8.4.2 스케줄링 가능성 분석
- 9. 고급 증명 기법
- 9.1 자동 증명 실패 시 대처 방안
- 9.1.1 증명기(Prover) 힌트 제공 (예: Assert, 유령 코드)
- 9.1.2 복잡한 계약 분리 및 재구성
- 9.2 외부 증명 보조 도구 활용
- 9.2.1 Why3 플랫폼 소개
- 9.2.2 SMT 솔버 (Alt-Ergo, CVC4/5, Z3) 연동
- 9.2.3 대화형 증명 보조 도구 (Coq, Isabelle/HOL) 연계 가능성
- 9.3 고급 유령 코드 기법
- 9.3.1 추상화 함수와 모델링
- 9.3.2 복잡한 데이터 구조 검증
- 9.4 부동소수점 연산 속성 증명
- 9.4.1 부동소수점 모델링 및 계약
- 9.4.2 오차 범위 분석 및 증명
- 9.1 자동 증명 실패 시 대처 방안
- 10. 저수준 프로그래밍 및 인터페이스
- 10.1 표현 명세(Representation Clause)
- 10.1.1 메모리 레이아웃 제어 (Pack, Size, Alignment)
- 10.1.2 하드웨어 주소 매핑 (Address)
- 10.2 C/어셈블리와의 인터페이스
- 10.2.1 Import, Export, Convention 프라그마
- 10.2.2 인터페이스 계약 및 검증 주의사항
- 10.3 휘발성(Volatile) 데이터 및 하드웨어 접근
- 10.3.1 Volatile 프라그마
- 10.3.2 MMIO(Memory-Mapped I/O) 처리
- 10.4 저수준 코드의 속성 증명
- 10.4.1 비트 수준 조작 검증
- 10.4.2 하드웨어 상호작용 모델링
- 10.1 표현 명세(Representation Clause)
- 11. 사례 연구 및 대규모 프로젝트 관리
- 11.1 사례 연구: 항공 전자 시스템 컴포넌트
- 11.1.1 요구사항 분석 및 SPARK 모델링
- 11.1.2 계약 정의 및 검증 과정
- 11.1.3 안전성 인증 고려 사항 (DO-178C 연계)
- 11.2 사례 연구: 보안 통신 모듈
- 11.2.1 보안 속성 정의 (기밀성, 무결성)
- 11.2.2 정보 흐름 분석 활용
- 11.2.3 Common Criteria 인증 연계
- 11.3 대규모 SPARK 프로젝트 관리 전략
- 11.3.1 팀 협업 및 코드 리뷰 프로세스
- 11.3.2 점진적 검증 및 통합 전략
- 11.3.3 도구 체인 자동화 및 CI/CD 연동
- 11.4 SPARK와 인증 표준
- 11.4.1 소프트웨어 안전성 표준 개요
- 11.4.2 SPARK가 인증 과정에 기여하는 방식
- 11.1 사례 연구: 항공 전자 시스템 컴포넌트
