설계를, 만들기 전에 검증합니다.

개발 중인 시스템, 또는 도입을 검토 중인 부품 하나를 대상으로 설계 단계의 검증을 수행합니다. 실물 장비는 필요하지 않습니다.

다만 검증을 하려면 설계를 읽어낼 수 있는 형태여야 합니다 —— 동작 조건, 상태, 인터록을 문서에서 추적할 수 있어야 합니다. 이 형태가 아닌 경우에는 설계서의 형식화를 앞 단계 작업으로 하여 별도로 견적해 드립니다.

장비 소프트웨어의 검증은 지금까지 통합 테스트와 현장 시운전까지 기다리는 수밖에 없었습니다. 진단은 그 기다림을 설계 단계로 끌어올립니다 —— 오류를 가장 싸게 고칠 수 있는 시점까지.

대상

개발 중인 시스템, 또는 도입 검토 중인 부품 하나. 검증 범위는 착수 전 협의로 확정합니다

기간

확정된 범위에 대해 4~8주가 기준입니다. 범위가 큰 경우에는 나누어 제안드립니다

조건

비밀유지계약(NDA) 체결. 설계 문서는 비공개로 취급합니다

비용

대상 규모에 따라 개별 견적

검증을 시작하려면 설계가 검증할 수 있는 형태여야 합니다. 그러나 현장의 설계서는 자연어로 쓰여 있고, 전제의 상당수는 숙련자의 머릿속에 있습니다. 이 옮겨 담는 수고가 형식기법의 실제 도입 장벽입니다.

이 작업을 저희가 맡습니다. 자연어로 된 설계서를 검증 가능한 사양의 형태로 옮기는 일 —— 이것 자체를 독립된 서비스로 제공합니다.

부수적인 효과

형식화된 설계서는 검증의 입력인 동시에 조직의 자산이 됩니다. 설계 노하우가 검증 가능한 형태로 바뀌면, 기술은 사람이 아니라 조직에 남습니다. 담당자의 이동이나 퇴사로 사라지던 암묵지가 읽을 수 있는 형태로 남습니다.

형식기법은 새로운 주장이 아닙니다. 주요 안전 규격은 최상위 안전 등급에서 이미 형식기법을 요구하거나 권고하고 있습니다.

리스크 평가에서 도출한 위험 시나리오를 모델화한 범위에서 “구조적으로 도달 불가능”하다고 증명하고, 그 증명과 근거를 인증 심사에 제출하는 자료의 일부로 쓸 수 있는 형태로 정리합니다. 인증 일정이 임박한 경우에는 검증 자체보다 이 문서가 더 급할 때가 있습니다.

제출 자료의 작성을 맡는 것이며, 인증의 가부 자체를 보장하지는 않습니다. 어느 규격의 어느 요구가 귀사의 장비에 적용되는지는 안전 등급과 용도에 따라 달라집니다. 그 판단은 인증 기관 또는 귀사의 안전 담당과 함께 확인합니다.

형식기법이 널리 쓰이지 않는 이유는 기술에 대한 의심이 아닙니다. 전문가 130명 대상 조사에서 71.5%가 “엔지니어의 교육 부족”을 최대 장벽으로 꼽았습니다. 필요한 것은 설득이 아니라 설명입니다.

커리큘럼의 뼈대는 “모델에서 검증으로 가는 한 단”입니다. 처음부터 가르칠 필요는 없습니다 —— 장비 엔지니어가 이미 알고 있는 모델 기반 개발 위에 “그 모델이 옳다고 증명한다”는 한 단을 얹는 데서 시작합니다.

진행 형태

사내 워크숍, 기술 세미나, 설계 리뷰 배석. 귀사의 장비를 소재로 삼을 수도 있고, 일반화한 예제로 시작할 수도 있습니다.

먼저 어떤 내용이 쓰여 있는지 읽어 보고 판단하고 싶으시다면 아티클을 공개하고 있습니다.