MALPAS 소프트웨어 정적 분석 도구 세트
MALPAS Software Static Analysis Toolset| 개발자 | 앳킨스 |
|---|---|
| 운영 체제 | 창문들 |
| 유형 | 정적 프로그램 분석 |
| 면허증 | 소유권 |
| 웹사이트 | www |
MALPAS는 엄격한 형태의 정적 프로그램 분석을 적용하여 소프트웨어의 정확성을 조사하고 증명할 수 있는 수단을 제공하는 소프트웨어 툴셋이다.도구는 분석 대상 프로그램을 나타내기 위해 지시된 그래프와 정규 대수학을 사용한다.분석가는 MALPAS에서 자동화된 도구를 사용하여 프로그램의 구조를 설명하고, 데이터의 사용을 분류하며, 입력 데이터와 출력 데이터 간의 정보 관계를 제공할 수 있다.그것은 또한 그 코드가 그 규격을 충족한다는 공식적인 증거를 뒷받침한다.
MALPAS는 원자력,[1] 항공우주[2] 및 방위[3] 산업에서 안전에 중요한 애플리케이션의 정확성을 확인하기 위해 사용되어 왔다.그것은 또한 사이즈웰 B에 대한 원자력 산업에서 컴파일러 유효성 검사를 제공하는 데 사용되었다.[4]분석된 언어는 다음과 같다.에이다, C, PLM, Intel Assembler.
MALPAS는 많은 프로그래밍 언어를 다루는데 있어 엄격하고 유연하기 때문에 원자로에 대한 컴퓨터 기반 보호 시스템에 대한 영국의 보건 안전 집행부 지침에서 요구하는 독립적인 정적 분석에 잘 적합하다.[5]
기술 개요
MALPAS 도구 세트는 프로그램의 다양한 속성을 다루는 5개의 특정 분석 도구로 구성된다.분석기에 대한 입력은 MALPAS 중간 언어(IL)로 작성해야 하며, 원본 소스코드의 자동 번역 도구에 의해 손으로 작성되거나 제작될 수 있다.자동 번역기는 Ada, C, Pascal과 같은 일반적인 고급 프로그래밍 언어뿐만 아니라 Intel 80*86, PowerPC, 68000과 같은 조립어에도 존재한다.IL 텍스트는 "IL 판독기"를 통해 MALPAS에 입력되며, 이는 분석 중인 프로그램에 대해 지시된 그래프와 관련 의미론을 구성한다.그래프는 일련의 그래프 감소 기법을 사용하여 축소된다.
MALPAS 툴 세트는 다음과 같은 5개의 분석기로 구성된다.[6]
- 제어 흐름 분석기.이것은 주요 특징인 진입/출입 지점, 루프, 지점 및 연결할 수 없는 코드를 식별하여 프로그램 구조를 조사한다.바람직하지 않은 구성에 주의를 끄는 요약 보고서와 프로그램 구조의 복잡성을 나타낸다.
- 데이터 사용 분석기.이것은 프로그램에 의해 사용되는 변수와 매개변수를 그 용도에 따라 구별되는 등급으로 구분한다. (즉, 쓰기 전에 읽는 데이터, 읽히지 않고 쓰는 데이터 또는 읽히지 않고 두 번 쓰는 데이터).보고서는 초기화되지 않은 데이터와 모든 경로에 기록되지 않은 함수 출력과 같은 오류를 식별할 수 있다.
- 정보 흐름 분석기.이것은 각 출력 변수나 파라미터에 대한 데이터 및 분기 의존성을 식별한다.코드를 통과하는 모든 경로에 대해 원하지 않거나 예상치 못한 종속성이 나타날 수 있다.사용되지 않은 변수와 중복 문장에 관한 정보도 제공된다.
- 의미 분석기(심볼릭 실행이라고도 함)이것은 코드를 통한 모든 의미론적으로 실현 가능한 경로에 걸쳐 모든 입력과 출력 사이의 정확한 기능 관계를 보여준다.
- 컴플라이언스 분석기.이것은 코드의 수학적 거동을 공식적인 IL 명세와 비교하며, 코드는 다른 코드와 다른 부분을 자세히 설명한다.IL 명세서는 선택적 코드 주장뿐만 아니라 전제조건과 포스트컨디션으로 작성된다.컴플라이언스 분석은 코드의 사양과 관련하여 코드의 기능적 정확성에 대한 매우 높은 수준의 신뢰를 얻기 위해 사용될 수 있다.
역사
도구 세트의 초기 연구와 초기 세대는 영국 말번(MALvern Programming Analysis Suite)에 있는 영국의 RSRE(Royal Signals and Radar Institute)에 의해 만들어졌다.1980년대 민간 핵과 무기 분야에서 광범위하게 사용되었는데, 당시 MALPAS 사용자 그룹을 설립한 렉스, 톰슨, 파트너스의 지원을 받았으며, 첫 번째 의장은 데이비드 H 스미스(2008년 현재 Frazer-Nash의 회장)이고, 이후 어드밴티지 테크니컬 컨설팅(2008년 Atkins가 인수)이 맡았다.
첫 번째 대규모 정적 분석 과제는 Sizewell B 발전소의 1차 원자로 보호 시스템에 있었다.이것은 재앙적인 실패에 대한 그것의 첫 방어선으로 컴퓨터 기반의 보호 시스템을 채택한 영국 최초의 원자력 발전소였다.여기에 체코의 CEZ는 테멜린 원자력 발전소의 원자로 보호 시스템에 대한 신뢰도를 높이기 위해 MALPAS를 채용했다.1995년 영국 왕립 공군은 안전성에 중요한 것으로 평가된 록히드 마틴 C130J의 항전 소프트웨어에 대한 독립적인 분석을 의뢰했다.MALPAS는 스파크 아다에서 작성되어 스파크 툴셋으로 검증한 미션 컴퓨터 소프트웨어와는 별도로 이 소프트웨어의 분석에 사용되었다.[7]
참조
- ^ 영국 NPP의 프로그램 가능 보호: 10년 후, D Pavey, British Energy.http://entrac.iaea.org/I-and-C/TM_VTT_2005_11/IAEA_papers/051124_Thursday/IAEA_paper_Pavey.pdf
- ^ C-130J 헤라클레스 안전 중요 소프트웨어에 대한 정적 코드 분석, Eur Ing K J Harrison, BSC CPhys MinstP CEng MRAeS MBCS; 영국 Aerosystems International, Aerosystems International. "Archived copy" (PDF). Archived from the original (PDF) on 2011-09-27. Retrieved 2011-03-18.
{{cite web}}: CS1 maint: 타이틀로 보관된 사본(링크) - ^ MALPAS 도구인 Hayman, K, Defense Sci. & Technol을 사용한 서드넌스 소프트웨어 분석.장기, 솔즈베리, SA. http://www.dsto.defence.gov.au/publications/scientific_record.php?record=9074
- ^ 소스 코드와 PROM 콘텐츠의 등가성에 대한 공식 시연, 신뢰할 수 있는 시스템의 수학에 관한 IMA 회의, 옥스퍼드 대학교 출판부, 1995, pp225248D J Pavy 및 L A Winsborrow
- ^ 컴퓨터 기반 안전 시스템 - 디지털 컴퓨터 기반 보호 시스템의 소프트웨어 측면 평가를 위한 기술 지침 : CS1 maint: 제목으로 보관된 사본(링크)
- ^ 정적인 분석에 대한 산업적 관점.소프트웨어 엔지니어링 저널 1995년 3월: 69-75위크만, B. A. A. 캐닝, D. L. 클루터벅, L. 윈즈버크, N. J. 워드, D.W. R. 마쉬http://www.ida.liu.se/~TDDC90/paper/industry95.pdf
- ^ C-130J 헤라클레스 안전 중요 소프트웨어에 대한 정적 코드 분석 : CS1 유지관리: 제목으로 보관된 사본(링크)
