- Introduction
– 어떠한 시스템을 구축하는 데에 있어서 하드웨어의 문제 보다는 종종 소프트웨어에서 결함이 발견되는 경우가 많다. 이러한 문제는 종종 시스템 전체에 치명적인 결과를 가져온다. 요즘의 소프트웨어 프로젝트는 그 규모가 점점 커지고, 더 복잡해지고 있으며, 그러한 프로젝트의 70% 정도는 예사 초과나 개발 기간 초과, 중도 개발 취소 등의 문제로 이어진다. 비록 성공적으로 평가 받는 소프트웨어 프로젝트들도 모든 요구 사항을 구현하지 못했거나 너무 많은 에러가 발생하는 등의 문제점을 안고 있다.
예를 들면, Praxis사의 이러한 문제점을 해결하기 위해 컴퓨터 분야에서는 이례적인 기술(수학적 로직(Logic) 정도로 볼 수 있는)과 최신 소프트웨어 공학 기술을 동시에 갖추고 있다. 그리고 소프트웨어 개발에 있어서 코드를 작성하는 것이 아닌, 프로그램의 로직을 나타내는 특수한 기호를 나열한다. 수학적 이론과 같이 이러한 기호의 나열은 그것이 논리적으로 올바르게 형성되어있는지 검증 받게 된다. 일단, 이렇게 작성된 것이 논리적인 결점을 포함하고 있지 않다고 검증되면 비로소 해당 기호의 나열이 프로그램 코드로 변환되게 된다. 이러한 방법은 실제 코드를 작성하기에 앞서서 버그를 제거하는 방법이다. Praxis사는 이러한 방법이 버그가 하나도 존재하지 않는 프로그램을 만들어 낸다고 주장하지는 않지만, 이 방법이 상당한 효과가 있다고 한다. Praxis사는 이 방법을 소프트웨어 개발에 적용한 결과, 산업 표준 보다 훨씬 좋은 버그 비율을 보이고 있다고 주장했다.
- Software was conceived as
– 과거와 달리, 소프트웨어 개발은 시간이 지남에 따라 점차 과학이라기보다는 기교에 가까워지고 있다. 또한, 최근의 소프트웨어 프로젝트는 점점 거대화, 복잡해지고 있다. 그리고 이러한 크고, 복잡한 소프트웨어 시스템은 일반적으로 불충분하게 구조화된 접근을 따르는 개발 팀을 압도 시킬만한 많은 모듈들을 포함하고 있다.
또한, 최근 조사에 의하면 IT프로젝트의 18%가 완성되지 못하고, 개발 도중에 취소가 되는데, 이는 10년 전의 31% 보다는 상황이 나아진 것이다. 그러나 여전히 씁쓸한 것은 현재의 수천개의 프로젝트들 중의 50% 이상은 문제에 직면해 있다는 것이다. 오직 28%의 프로젝트만이 엄격한 정의에 의해 납득할만한 성공을 거두었다.
오늘날, 소프트웨어 프로젝트의 모든 측면을 관리하는 기업을 지원하기 위해 많은 복잡한 도구들이 사용되고 있다. 이러한 툴들은 시스템을 디자인하고, 개념화하는 것을 돕는다. 현재 이러한 소프트웨어 개발 도구들의 전세계적인 판매는 매년 3조원을 넘는다. 그러나 이러한 소프트웨어들의 질적인 면은 상세하고 정밀하게 측정되지 못하고 있다. (이와 관련된 예로 Praxis사의 전자칩이 내장된 전자 지갑에 대한 실례가 기사문에 포함되어 있다.)
- The Praxis team began working
– Praxis사의 개발 팀에 관한 이야기가 계속되며, Praxis사에서 개발에 사용하는 언어(Language)에 대한 이야기이다. Praxis사는 요구 명세서 등 여러 개발 관련 문서를 작성하기 위해 Z라는 특수어를 사용한다. 이는 엄밀히 프로그래밍 언어가 아니지만, 어떠한 증명을 쉽게 이끌어 낼 수 있는 어떠한 개념을 표현하도록 돕는 일반 명세 언어이다. 이 언어는 모순이나 모호함을 사전에 차단하고, 실제 소프트웨어를 만들기 전에, 개발자들이 버그와 관련된 문제를 사전에 해결하도록 한다.
사실 이러한 개발 과정은 시간이 많이 소모되는 일로, 전체 개발 과정의 약 25% 정도를 차지한다고 한다. 이 시간 비중은 실제 생산된 어떠한 결과물도 없이 보내기에는 상당히 오랜 시간이라 말할 수 있다. 그러나 이는 시간 낭비가 아니라고 Praxis사의 프로젝트 관계자는 밝히고 있다. 대부분의 프로젝트가 초기에 완벽한 계획과 준비 없이 바로 코딩에 들어가는 경우가 많은데, 이는 오히려 개발에 들어가서 개발자들을 더 어렵게 하고, 더 많은 예산 낭비를 가져온다. 완벽한 초기 단계의 준비와 설계를 위해서는 많은 시간의 투자를 요하지만, 그 효과는 실제 개발에 들어가서 볼 수 있게 된다.
이렇게 초기 개발 단계에서 Z언어를 사용하여 작성된 개발 관련 문서는 다시 Spark라 불리는 프로그래밍 언어를 통해서 실제 컴퓨터 코드로 변환된다. Praxis사에서 쓰이는 이 Spark라는 언어는 많은 일반 프로그래밍 언어가 가지고 있는 표현의 모호함이 존재하지 않는다. 결국, 이러한 모호한 표현으로 발생되는 에러 자체가 초기에 차단되므로 에러 발생률이 상당히 줄어들게 된다.
이러한 단계(English -> Z -> Spark)를 거치는 동안, 개발자들은 개발 상에서 발생하는 언어간의 의미상 차이의 큰 갭(Gap)을 느끼지 않으며, 다른 추가 작업(컴파일, 러닝)없이 프로그램 특정 속성을 분석할 수 있게 된다.
이렇게 Praxis사는 이러한 개발 과정을 도입함으로써, 버그 발생율을 획기적으로 감소시켰으며, 실제 테스트에서 필요한 노력을 줄임으로써, 전체적인 개발 비용을 줄이고 있다. 그들은 버그 발생 비율을 줄이면 줄일수록 개발에 필요한 인력과 비용을 아낄 수 있다고 한다.
- Formal Methods were relatively new
최근 들어 Microsoft와 같은 대기업들도 개발 중에 발생하게 되는 버그로 인해 불필요하게 낭비되는 비용을 최소화하고자 Formal Method(또는 이러한 방법을 제공하는 툴, ex) Z, Spark)을 작은 프로젝트에 투입하고 있다. 그러나 이러한 툴이 아직은 일반적인 개발자들에게는 적합하지 않으며, 완전한 컴퓨터 과학 학위를 따거나 순수 수학에 능숙한 소수의 사람들에게만 유용하다고 한다. 하지만 이러한 Formal Method는 점점 많은 개발자들에게 사용이 쉽도록 변화하고 있으며 많은 기업이나 정부 기관에서도 버그를 줄이기 위해 이러한 시스템을 도입하고 있다.
마지막으로 덧붙이자면 Praxis사의 관계자는 아직까지는 모든 문제들이 Formal Method로 쉽게 해결되는 것은 아니라고 한다. 현재 가장 중요한 걸림돌은 프로젝트의 규모이다. 규모가 상당히 커지게 된다면 Formal Method의 적용은 어려워진다. Praxis사는 그들의 프로젝트는 절대 큰 규모가 되지는 않을 것이라 하지만, 결과야 어찌 될 것인지 간에 Formal Method는 점차 대규모 프로젝트에도 적합하도록 발전할 것으로 믿고 있다고 한다. 그들은 이 문제의 해결책으로 추상화(Abstraction)를 이야기 학 있는데, 프로젝트 개발에 있어서 충분한 추상화 과정이 이루어 질 수 있게 된다면, 대규모의 프로젝트도 쉽게 다룰 수 있을 정도의 크기로 잘게 쪼개어 작업을 진행 시킬 수 있게 될 것이라고 한다.