아티클

형식기법을, 장비 엔지니어의 언어로

형식기법의 가장 큰 장벽은 어려움이 아니라 낯섦입니다. 전문가 130명 대상 조사에서 71.5%가 “엔지니어의 교육 부족”을 도입의 최대 장벽으로 꼽았습니다. 그래서 저희는 영업보다 설명을 먼저 놓습니다.

순서대로 읽으면 장비 소프트웨어의 검증 공백에서 시작해, 형식기법이 그 공백을 어떻게 메우는지까지 하나로 이어지도록 썼습니다. 어디부터 읽으셔도 괜찮습니다.

  1. 01 기초

    왜 장비 소프트웨어는 V자 모델의 오른쪽 절반을 실행할 수 없는가

    장비 개발 현장이 "돌아가면 됐다"로 수십 년을 버텨온 것은 대충 해서가 아닙니다. 단위 테스트가 물리적으로 성립하지 않는 구조였기 때문입니다.
  2. 02 기초

    "모델로 설계한다"의 다음에 오는 것

    세계는 이미 문서가 아니라 모델로 설계하기 시작했습니다. 그러나 그 모델이 옳은지에 대해서는 어떤 도구도 답하지 않습니다. 그 공백에 관한 이야기입니다.
  3. 03 기초

    테스트와 형식기법은 무엇이 다른가

    테스트는 시험해 본 범위를 확인하고, 형식기법은 일어날 수 있는 모든 상태를 확인합니다. 그 차이가 드러나는 곳은 테스트에서는 나오지 않고 현장에서 나오는 한 무리의 버그입니다.
  4. 04 실무

    반례란 무엇인가

    설계 검증이 문제를 찾아냈을 때 돌아오는 것은 경고가 아니라, 위반을 재현하는 구체적인 이벤트 시퀀스입니다. 그것을 현장에서 어떻게 쓰는지 적습니다.
  5. 05 규격

    왜 안전 규격은 형식기법을 요구하는가

    형식기법은 새로 나온 세일즈 문구가 아닙니다. IEC 61508도 DO-178C도, 안전 등급이 올라간 지점에서 형식기법을 지목하고 있습니다. 그 이유를 적습니다.
  6. 06 사례

    누가 실제로 쓰고 있는가

    형식기법을 실제로 쓰고 있는 조직과 그 사용 방식을 짚습니다. 아울러 보급이 어디까지 진행되지 않았는지도 있는 그대로 적습니다.

귀사의 설계로 확인해 보시겠습니까.

아티클은 일반적인 설명입니다. 귀사의 장비에서 실제로 무엇이 나오는지는, 대상을 하나 정하면 알 수 있습니다.

문의하기