2016년 1월 17일 일요일

TDD, BDD를 넘어서 - 검증 주도 개발(Verification-Driven Development,VDD)에 대하여

최근 진행한 나는 프로그래머다 녹음에서는 서울대학교 컴퓨터 공학부의 이광근 교수님을 모시고 최근 저술하신 책 - 컴퓨터과학이 여는 세계와 학문으로서의 컴퓨터 과학을 주제로 방송을 진행하였다. 임작가님이 3연휴를 희생하여 편집에 의욕을 보여 주신 덕분에 빠르게 공유될 수 있지 않을까 기대해 본다. (블로그 글을 작성하고 있는 도중에 편집본이 도착했다 ^^)

방송 말미에 앞으로 교수님께서 주목하고 있는 언어 관련 최신 동향에 대해서 소개를 부탁드려 봤는데 그때 말씀해 주신것이 지금부터 소개하려 하는 정확한 검증(formal verification)이다. 아직은 학문적 영역에 머물러 있지만 조만간(이교수님 말씀으로는 5년) 우리 앞에 모습을 드러 낼 수 있을것으로 보이기에 어떠한 것인지를 현업 개발자의 시선에서 설명해 보고자 한다.

정확한 검증(formal verification) 과 정확한 사양(formal specification)


정확한 검증이란,  하드웨어 및 소프트웨어 시스템에서 정형기법과 같은 수학 논리를 이용하여 어떤 정확한 사양 기술 및 속성에 비추어 시스템이 올바른지를 증명 하거나 반대로 잘못된 것을 증명하는 것을 말한다. 구현하고자 하는 대상을 정확한 검증이 가능하도록 기술하는 것을 명세 언어(Specification language)라 하는데 대표적인 명세언어는 우리가 개발에서 흔히 사용하는 UML이 있다.

정확한 검증이 도입되면 대상 시스템이 명세 언어로 작성된 사양에 비추어 올바른지 여부를 자동으로 판정하는 것이 가능해진다. 이를 통해 개발 과정에서 구현과 동시에 사양에 대한 검증을 실시하는것이 가능해 진다. 

정확한 검증의 필요성은 설계 (또는 구현)의 '정당성'은 그 자체만으로 확인할 수 없다는 점에서 출발한다. 정당성은 주어진 사양과의 검증을 통해 처음으로 확인 가능하며, 정확한 사양의 표기가 해결해야 할 문제를 제대로 설명 할 수 있는지 여부는 또 다른 문제이다. 이것 또한 어려운 문제이며, 비 형식적인 실제 문제를 추상화 된 형식적인 사양 기술에서 제대로 설명해야 하는 문제에 귀착한다. 이러한 요약(abstraction)은 증명이 불가능하다. 그러나 사양에 대한 정리 를 증명할 수 있다면, 사양의 무결성을 검증하는 것은 가능하다. 

 검증에 대한 개요. 구현과 사양의 개발이 함께 진행되고 최종적으로는 툴에 의한 검증이 이루어 진다는 점에 주목하자.  이미지 출처: OS Verification -- Now! 


현재 현업 개발현장에서 사용되고 있는 일반적인 자동화 검증 기법은 다음과 같은 것 들이 있다.

  • 단위 테스트(Unit test) : 함수(또는 메소드)단위로 테스트 코드를 작성하여 실시하는 자동화 테스트. 반복개발 프로세스 안에서 단위 테스트를 구현과 묶어서 개발 하는 방법론을 테스트 주도 개발(Test-Driven Development,TDD)이라 부른다.
  • 행위 테스트(Behavior test) : 테스트 범위를 함수 단위에서 기능단위로 확장시킨 테스트형태를 말하며 테스트가 사양 명세(Specification) 그 자체가 되는것을 목표로 하기때문에 테스트 코드의 작성에는 자연 언어에 가까운 도메인 고유 언어(DSL)가 선호된다.  TDD와 마찬가지로 개발 프로세스에 행위 테스트 작성을 프로세스의 일부로서 도입한 개발 형태를 행위 주도 개발(Behavior-Driven Development,BDD)이라 부른다.
  • End-To-End 테스트(e2e test): 독립적으로 작동하고 Mock와 Stub를 사용하는 BDD 나 단위 테스트와는 반대로,  End-to-End 테스트는 가능한 한 실제 시스템의 사용자에 가깝게 에뮬레이션하려고한다. 대표적인 툴 로는 Selenium 이 있다.

자동화 테스트와의 차이

 위에서 소개한 자동화 테스트들이 정해진 숫자의 테스트 케이스만을 소화해 내는 형태인데 비해 정확한 검증은 구현된 로직 자체가 사양과 일치 하는지를 검증해 내고자 한다. 실제로 TDD를 이용해 개발을 해 본 개발자라면 사람이 예상한 테스트 케이스와 실제 동작에서 발생하는 경우의 수 사이에 늘 차이가 존재 할 수 밖에 없다는 사실에 동의할 것이다. 설사 많은 노력을 투입하여 모든 경우의 수를 커버하는 테스트 케이스를 작성한다 할 지라도 그것이 애초에 구현하고자 한 대상과 동일한 것이라는 사실을 보장해 주지 못한다. 이상적인 정확한 검증의 구현은 사양 자체가 검증과 일체화 되기 때문에 구현에 대한 버그가 발생하게 될 여지가 존재하지 않는다. 이러한 점은 BDD가 이루고자 하는 목표와도 일치한다.

정확한 검증 방법

정확한 검증은 크게 두 가지로 분류된다.


모델 검사

첫 번째 방법인 모델 검사는 수학적 모델을 통해 체계적이고 철저하게 검증하는 것을 말한다. 여기서 말하는 모델은 유한 상태 모델을 지칭 하지만 무한의 상태를 가지는 모델도 추상화를 통해 유한 표현으로 전환이 가능하다면 확인 가능한 모델로 취급한다. 일반적으로 모델의 전체 상대와 전체 상태 전환의 검증을 포함하며, 연산 시간을 줄이기 위해 영역고유의 추상화 기법을 이용하여 효율화를 도모한다.

다만, 모델 검사는 하드웨어 설계에 적용되는 경우가 많고 소트웨어에 대한 모델 검사는 결정 불능이므로 알고리즘적인 방법만으로는 완전하지 않고, 증명도 반증도 할 수 없는 경우가 있다. 모델검사에 사용되는 방법으로는 선형시상논리(Linear Temporal Logic,LTL)나 계산 트리 논리(Computational Tree Logic, CTL)가 있다. (솔직히 나 자신은 이 글을 작성 하면서도 위의 링크를 눌러 볼 엄두가 안난다.)

논리적 추론

두 번째 방법은 논리적 추론이다. 일반적으로 엄밀한 논리 추론을 돕는 자동도구(Automated Theorem Proving, ATP) 소프트웨어를 사용하여 시스템에 관한 정확한 추론을 실시한다. 이 기술은 완전 자동화 되어있지 않은것이 일반적이었으나 최근들어 Perfect Developer와 Escher C Verifier와 같은 도구가 등장하여 증명에 대한 완전 자동화를 시도하고 있다. 

Java Modeling Language(JML)과 Spec#

학교와 연구소에서 벗어난 정확한 검증이 우리 앞에 어떠한 모습으로 나타날까? Java Modeling Language(JML)과 Spec#은 논리적 추론을 통해 정확한 검증을 구현하려는 프로젝트이다. 어노테이션에 검증을 위한 사양을 JMS 사양 이라는 표기법으로 기술한다.

이해를 돕기 위해 위키사전에 실려 있는 JML 의 예제를 살펴보자.

public class BankingExample
 {
 
    public static final int MAX_BALANCE = 1000; 
    private /*@ spec_public @*/ int balance;
    private /*@ spec_public @*/ boolean isLocked = false; 
 
    //@ public invariant balance >= 0 && balance <= MAX_BALANCE;
 
    //@ assignable balance;
    //@ ensures balance == 0;
    public BankingExample()
    {
        this.balance = 0;
    }
 
    //@ requires 0 < amount && amount + balance < MAX_BALANCE;
    //@ assignable balance;
    //@ ensures balance == \old(balance) + amount;
    public void credit(final int amount)
    {
        this.balance += amount;
    }
 
    //@ requires 0 < amount && amount <= balance;
    //@ assignable balance;
    //@ ensures balance == \old(balance) - amount;
    public void debit(final int amount)
    {
        this.balance -= amount;
    }
 
    //@ ensures isLocked == true;
    public void lockAccount()
    {
        this.isLocked = true;
    }
 
    //@   requires !isLocked;
    //@   ensures \result == balance;
    //@ also
    //@   requires isLocked;
    //@   signals_only BankingException;
    public /*@ pure @*/ int getBalance() throws BankingException
    {
        if (!this.isLocked)
        {
                return this.balance;
        }
        else
        {
                throw new BankingException();
        }
    }
 }

cucumber나 RSpec을 접해본 독자라면 위와 같은 표기법이 낮설지 않을것이다.

이번에는 마이크로소프트의 연구소에서 연구중인 Spec#의 예제를 살펴보자. 아래 예제는 C#에 기술된 Spec#이다.

static void Main(string![] args)
        requires args.Length > 0;
    {
        foreach(string arg in args)
        {
            Console.WriteLine(arg);
        }
    }

'requires args.Length > 0;'이 Spec#의 구문으로 자바에서 흔히보는 Assertion과 흡사하다. 위 예제는 설명을 위해 단순한 값에 대한 검증만을 기술하고 있지만 API레벨에서 이뤄지는 복잡한 동기화에 대한 기술도 가능하다.
Spec#에 대해 좀 더 자세히 알고 싶으신분은 공식 사이트를 방문해 보시길 권한다.

멀티코어,비동기, 동시성, 함수형 그리고 검증 주도 개발(Verification-Driven Development,VDD)

필자가 정확한 검증에 주목하는 이유는 유닛테스트나 e2e테스트와 같은 기존의 테스트 패러다임으로는 동시성과 관련하여 발생하는 오류를 찾아내기가 힘들기 때문이다. 오늘날의 컴퓨팅 한경은 멀티코어가 일반화 됨에 따라 이에 대응하기 위한 비동기, 동시성 프로그래밍 패러다임이 출연하였다. 그리고 이를 보다 효과적으로 구현하기 위한 함수형 프로그래밍은 본격적으로 하나의 큰 흐름을 시작하고 있는 단계이다. 비동기 프로그래밍의 가장 큰 난관으로 꼽히는 것은 테스트의 어려움이다. 발생할 수 있는 경우의 수에 대한 파악도 어렵고 재현도 어렵기 때문이다. 이제 막 보급되기 시작한 이러한 새로운 개발 패러다임 에는 테스트의 복잡도 제어와 효율적인 검증이라는 큰 숙제가 여전히 남겨져 있는 상태인 것이다.
하지만 만약에 코드 자체가 스스로의 완전성을 보장해 준다면 어떨까?
정확한 검증이 그 대안이 되어 줄 수 있지 않을까? 꿈같은 이야기로 들릴지 모르지만 어차피 지금 우리들이 사용하는 기술들은 과거엔 마법같이 여겨지던 것들이다.
이교수님의 말씀처럼 가까운 실일내에 정확한 검증 기술이 상용 코드에 적용 가능한 수준으로 성숙된다면 BDD를 넘어서서 검증 주도 개발(VDD)이라는 패러다임이 등장할 수도 있다는 것이 필자의 생각이다.

필자의 의견으로는 지금 현업에 있는 대부분의 프로그래머에게 있어 당장 정확한 검증을 익혀두거나 도입을 서두를 필요는 없을것이라 본다. 다만, Cucumber와 같이 트레이드 오프에 대한 검증이 끝난 BDD 프레임웍의 도입은 DevOps시대를 맞이하여 효율적인 품질관리와 생산성 증대를 위해서라도 살펴봐 두는 자세가 필요할 것이다.


참고 문헌 & 관련 링크


※이광근 교수님의 피드백을 받아 학술 용어의 번역에 대해서 수정을 하였습니다.(2016.1.17)


시간:

댓글 없음:

댓글 쓰기

피드 구독하기: 댓글 (Atom)