Safety-Critical 소프트웨어 종합 솔루션 파트너
안전·보안·품질을 코드로 구현합니다
원전, 자동차, 국방, 산업제어 등 safety-critical 시스템 소프트웨어를 대상으로, 검증·성능·보안을 아우르는 종합 솔루션을 제공합니다.
회사 소개
2007년 설립, Safety-Critical 소프트웨어 전문 기업
포멀웍스는 원전, 자동차, 국방·항공우주, 산업제어 등 safety-critical 시스템 소프트웨어의 검증·품질·보안을 전문으로 하는 기술 기업입니다. 소프트웨어 검증(V&V), 실시간 성능 분석(WCET), 사이버보안 평가, 임베디드 소프트웨어 종합 분석 도구(HKSAT), 블록체인 DID 기반 출입통제(FOR PASS-M), AR/VR 기반 지휘통제·훈련 시스템 등 다양한 솔루션과 서비스를 제공합니다.
비전
“기술로 더 인간다운 삶을 구현하는 것”
정직
제품과 서비스의 품질을 최우선에 두는 전문성과 책임감
기술
수준 높은 제품과 서비스를 제공하기 위한 개인과 조직의 역량 강화
인간존중
사람을 최우선으로 생각하며 임직원이 일을 즐길 수 있는 환경
사업·서비스
코드 수준에서 안전과 신뢰를 보장하는 기술 파트너
소프트웨어 검증(V&V)
IEEE 1012, IEC 61508, ISO 26262, KEPIC-S-9 등 국제·국내 표준 기반 소프트웨어·시스템 검증
안전성·보안성 평가
원전 사이버보안 평가, 자산·취약점·위협·위험 분석 기반 보안 평가 프레임워크(NUSAF 등)
실시간 성능·WCET 분석
HKSAT를 활용한 원전·자동차 ECU·전장 소프트웨어 최장 수행 시간(WCET) 분석
검증·보안 도구 개발 및 컨설팅
HKSAT 등의 자체 검증 도구 및 관련 컨설팅, 개발 프로세스·CI/CD·표준 준수·규제 대응 지원
주요 적용 분야
제품 소개
자체 개발 솔루션 및 플랫폼
HKSAT
임베디드 소프트웨어 종합 분석 도구
HKSAT는 임베디드 소프트웨어의 안전성·성능·변경 영향을 한 번에 분석하는 통합 검증 플랫폼입니다. C/C++ 소스 코드를 대상으로 정적 분석, WCET, 스택·스케줄 분석, 변경 영향 분석 등을 하나의 플랫폼에서 수행합니다.
정적 분석 (SSAT)
API 사용 규칙 준수, 재귀, 전역 변수, 경쟁 조건 등 검출
WCET 분석
실시간 태스크 시간 제약 충족 여부 판단
스케줄 가능성 분석 (SCHA)
실시간 태스크 스케줄링 가능 여부 분석
스택 사용량 분석 (SSUA)
스택 오버플로 사전 식별
변경 영향 분석 (SCIA)
코드 변경에 따른 재시험·재검증 범위 추적
중복 코드 분석 (DBCA)
유지보수·보안 리스크 감소를 위한 중복 코드 탐지
프로젝트 사례
국내외 안전-중요(safety-critical) 분야에서 검증된 파트너
신울진 원전 1·2호기 및 수출 원전 안전등급 V&V
원전 안전등급 계통의 소프트웨어·시스템 요구사항·설계·코드·테스트 전 과정에 대한 표준 기반 검증 수행
POSAFE-Q 안전등급 제어기기 검증·보안 분석
소프트웨어·하드웨어 통합 검증, 안전성 분석 및 사이버보안 평가, 국내 인허가 대응
원전 사이버보안 평가(NUSAF)
자산·취약점·위협·위험 분석 기반 사이버보안 평가 방법론 구축 및 규제·인허가 대응 지원
현대·기아자동차 공동 특허 및 기술 협업
자동차 ECU·전장 소프트웨어에 대한 실시간 성능·WCET 분석 및 V&V 수행
FOR PASS-M 군부대·공공 출입통제 실증
육군사관학교, 국방부, 서울시 테스트베드 사업을 통해 모바일 DID 출입관리 체계 실증
국방 AI + XR 해커톤·R&D 참여
한화시스템, LIG넥스원, 방사청 등과 LLM·Multi-RAG 활용 AI 기반 전략·의사결정 지원 과제 수행
방산혁신기업 100
2024년 방위사업청 주관 방산혁신기업 100에 3기로 선정
연락처
문의사항이 있으시면 언제든지 연락해 주세요
Tel
02-563-8763
Fax
02-563-8764
contact@formalworks.com
서울특별시 서초구 반포대로 110, 산우빌딩 5층
서초역 2번 출구에서 도보 3분
