안전에 중요한 소프트웨어에는 어떤 언어가 사용됩니까?

안전에 중요한 소프트웨어에는 어떤 언어가 사용됩니까? [닫은]

---

안전에 중요한 소프트웨어의 개발을 연구하고 있으며 특히 프로그래밍 언어의 선택이 그러한 개발에 어떤 영향을 미치는지 연구하고 있습니다.

일반적으로 사용되는 언어와 그 이유를 자세히 설명하십시오.

---

항공 전자 시스템과 같은 고 신뢰성 소프트웨어를 구축하기 위해 Ada 및 SPARK (정적 검증을위한 일부 후크가있는 Ada 방언)가 항공 우주 서클에 사용됩니다. 의 뭔가가 다음 언어에 대한 코드 검증 툴의 생태계는 이 기술이 또한 존재하지만, 뿐만 아니라 주류 언어 .

Erlang 은 처음부터 신뢰성이 높은 통신 코드 를 작성 하도록 설계되었습니다 . 오류 복구에 대한 우려를 쉽게 분리 할 수 ​​있도록 설계되었습니다 (즉, 오류를 생성하는 하위 시스템이 오류를 처리하는 하위 시스템과 다름). 이 기능이 실제로 연구 분야에서 멀어지지는 않았지만 공식적인 증거를받을 수도 있습니다.

Haskell 과 같은 기능적 언어 는 언어 의 선언적 특성 으로 인해 자동화 된 시스템에 의해 공식적인 증거를받을 수 있습니다 . 이를 통해 부작용이있는 코드를 모나 딕 함수에 포함시킬 수 있습니다. 공식적인 정확성 증명을 위해 나머지 코드는 지정된 것 외에는 아무것도하지 않는 것으로 가정 할 수 있습니다.

그러나 이러한 언어는 가비지 수집되고 가비지 수집은 코드에 투명하므로 이러한 방식으로 추론 할 수 없습니다. 시간 제한 증분 가비지 수집기에 대한 지속적인 연구가 있지만 가비지 수집 언어는 일반적으로 어려운 실시간 응용 프로그램에 대해 충분히 예측할 수 없습니다.

Eiffel 과 그 자손은 불변 인에 대한 사전 및 사후 점검을 통합하기위한 강력한 런타임 메커니즘을 제공하는 Design By Contract 라는 기술을 기본적으로 지원합니다 . Eiffel은 실제로 따라 잡지는 못했지만, 고 신뢰성 소프트웨어를 개발하는 것은 실제로 기능을 작성하기 전에 장애 모드에 대한 사전 점검 및 처리기 작성으로 구성되는 경향이 있습니다.

하지만 C 와 C ++는 특별히 이러한 유형의 애플리케이션을 위해 설계되지 않은, 그들은 널리 여러 가지 이유로 임베디드 및 안전에 중요한 소프트웨어에 사용됩니다. 메모의 주요 속성은 메모리 관리 (예를 들어 가비지 수집을 피할 수 있도록 함), 간단하고 잘 디버깅 된 코어 런타임 라이브러리 및 성숙한 도구 지원입니다. 오늘날 사용되는 많은 임베디드 개발 툴 체인은 현재 기술이었던 당시 1980 년대와 1990 년대에 처음 개발되었으며 당시 유닉스 문화에서 왔기 때문에 이러한 툴은 이런 종류의 작업에 인기를 유지합니다.

오류를 피하기 위해 수동 메모리 관리 코드를주의 깊게 검사해야하지만 가비지 수집에 의존하는 언어로는 사용할 수없는 응용 프로그램 응답 시간을 어느 정도 제어 할 수 있습니다 . C 및 C ++ 언어 의 핵심 런타임 라이브러리 는 비교적 단순하고 성숙하며 잘 이해되어 있으므로 가장 안정적인 플랫폼 중 하나입니다. Ada에 사용 된 모든 정적 분석 도구가 C 및 C ++도 지원하지는 않지만 C에 사용할 수있는 다른 도구 가 많이 있습니다 . 있습니다 또한 여러 널리 사용되는 C / C ++ 기반의 툴 체인 ; Ada에 사용되는 대부분의 툴 체인은 C 및 / 또는 C ++를 지원하는 버전으로 제공됩니다.

Axiomatic Semantics (PDF), Z Notation 또는 Communicating Sequential Process 와 같은 공식적인 방법을 사용하면 프로그램 논리를 수학적으로 확인할 수 있으며 응용 프로그램이 적용하기에 충분히 간단한 안전 핵심 소프트웨어 (일반적으로 임베디드 제어 시스템)의 설계에 자주 사용됩니다. . 예를 들어 전 강사 중 한 명이 독일 철도 네트워크의 신호 시스템에 대한 공식적인 정확성 증명을 수행했습니다.

공식적인 방법의 주요 단점은 입증 된 기본 시스템과 관련하여 기하 급수적으로 복잡 해지는 경향입니다. 이는 증명에 오류가 발생할 위험이 매우 높기 때문에 사실상 간단한 응용 프로그램으로 제한됩니다. 하드웨어 버그는 특히 대량 시장 제품에서 수정하는 데 비용이 많이 들기 때문에 공식적인 방법은 하드웨어 정확성을 검증하는 데 널리 사용됩니다. Pentium FDIV 버그 이후 공식적인 방법은 많은 주목을 받았으며 Pentium Pro 이후 모든 인텔 프로세서 에서 FPU의 정확성을 확인하는 데 사용 되었습니다 .

많은 다른 언어가 신뢰성이 높은 소프트웨어를 개발하는 데 사용되었습니다. 이 주제에 대해 많은 연구가 이루어졌습니다. 특정 플랫폼의 사용을 방해 할 수있는 종속성의 단순성 및 선택 및 제어와 같은 원칙이 있지만 방법론이 플랫폼보다 중요 하다고 합리적으로 주장 할 수 있습니다 .

다른 여러 플랫폼에서 언급했듯이 특정 O / S 플랫폼에는 워치 독 타이머 및 보장 된 인터럽트 응답 시간과 같은 안정성과 예측 가능한 동작을 촉진하는 기능이 있습니다. 단순성은 또한 강력한 신뢰성의 원동력이며, 많은 RT 시스템은 의도적으로 매우 단순하고 컴팩트하게 유지됩니다. QNX (내가 유일하게 익숙한 유일한 O / S를 기반으로 한 구체적인 배치 시스템 으로 작업 한 적이 있음)는 매우 작으며 단일 플로피에 맞습니다. 비슷한 이유로 강력한 보안 및 철저한 코드 감사로 알려진 OpenBSD 를 만드는 사람들 도 시스템을 단순하게 유지합니다.

편집 : 이 게시물 에는 안전에 중요한 소프트웨어, 특히 Here and Here 에 대한 좋은 기사로 연결되는 링크가 있습니다. S.Lott 및 Adam Davis에게 소스를 제공합니다. THERAC-25 의 이야기는 이 분야에서 약간의 고전적인 작품입니다.

---

C ++의 경우 Joint Strike Fighter (F-35) C ++ 코딩 표준을 잘 읽어보십시오.

http://www.stroustrup.com/JSF-AV-rules.pdf

---

저는 Ada 가 안전 및 / 또는 미션 크리티컬 한 일부 정부 프로젝트에서 여전히 사용되고 있다고 생각 합니다. 나는 언어를 사용한 적이 없지만 에펠과 함께 "배우기"목록에 있습니다. Eiffel은 Design By Contract를 제공하며 안정성과 안전성을 향상시킵니다.

---

첫째, 안전에 중요한 소프트웨어는 고전적인 기계 및 전기 공학 분야에서 볼 수있는 것과 동일한 원칙을 준수합니다. 중복성, 내결함성 및 페일 세이프티.

따로 그리고 이전 포스터가 암시하고 어떤 이유로 다운 투표를했다고해서이를 달성 할 수있는 가장 중요한 요소는 팀이 진행중인 모든 사항을 확실하게 이해하는 것입니다. 좋은 소프트웨어 디자인이 핵심이라는 것은 말할 것도 없습니다. 그러나 그것은 또한 접근 가능하고, 성숙하며, 잘 지원되는 언어를 의미하며, 여기에는 많은 공동 지식과 경험이 풍부한 개발자가 있습니다.

많은 포스터는 이미 OS가 결정 론적이어야하기 때문에 가장 진실한 핵심 요소라고 이미 언급했습니다 (QNX 또는 VxWorks 참조). 이것은 당신을 위해 무대 뒤에서 일을하는 대부분의 해석 언어를 배제합니다.

ADA는 가능성이 있지만 도구와 지원이 적으며 더 중요한 사람들은 쉽게 구할 수 없습니다.

C ++은 가능성이 있지만 하위 집합을 엄격하게 적용하는 경우에만 가능합니다. 이런 점에서 그것은 악마의 도구이며, 우리의 삶을 더 편하게 해줄 것을 약속하지만 종종 너무 많은 일을합니다.

C가 이상적입니다. 매우 성숙하고 빠르며 다양한 도구 및 지원 세트가 있으며 많은 숙련 된 개발자, 크로스 플랫폼 및 매우 유연하며 하드웨어와 가까이서 작업 할 수 있습니다.

나는 스몰 토크에서 루비에 이르기까지 모든 것을 개발했으며 더 높은 언어가 제공하는 모든 것을 높이 평가하고 즐긴다. 그러나 중요한 시스템 개발을 할 때 총알을 깨물고 C로 고수합니다. 내 경험 (방어 및 많은 클래스 II 및 III 의료 기기)에서 더 적습니다.

---

다른 모든 것보다 안전하다면 하스켈을 집어 들었습니다. 저는 매우 엄격한 정적 유형 검사 기능을 가지고 있으며 테스트하기 쉬운 방식으로 부품을 제작하는 프로그래밍을 촉진하기 때문에 haskell을 제안합니다.

But then I wouldn't care about language much. You can get much greater safety without compromising as much by having your project overall in condition and working without deadlines. Overall as in having all the basic project management in place. I'd perhaps concentrate on extensive testing to ensure everything works like it ought, tests that cover all the corner cases + more.

---

The language and OS is important, but so is the design. Try to keep it bare-bones, drop-dead simple.

I would start by having the bare minimum of state information (run-time data), to minimize the chance of it getting inconsistent. Then, if you want to have redundancy for the purpose of fault-tolerance, make sure you have foolproof ways to recover from the data getting inconsistent. Redundancy without a way to recover from inconsistency is just asking for trouble.

Always have a fallback for when requested actions don't complete in a reasonable time. As they say in air traffic control, an unacknowledged clearance is no clearance.

Don't be afraid of polling methods. They are simple and reliable, even if they may waste a few cycles. Shy away from processing that relies solely on events or notifications, because they can be easily dropped or duplicated or misordered. As an adjunct to polling, they are fine.

A friend of mine on the APOLLO project once remarked that he knew they were getting serious when they decided to rely on polling, rather than events, even though the computer was horrendously slow.

P.S. I just read through the C++ Air Vehicle standards. They are OK, but they seem to assume that there will be lots of classes, data, pointers, and dynamic memory allocation. That is exactly what there should no more of than absolutely necessary. There should be a data structure czar with a big scythe.

---

The OS is more important then the language. Use a real time kernel such as VxWorks or QNX. We looked at both for controlling industrial robots and decided to go with VxWorks. We use C for the actual robot control.

For truly critical software, such as aircraft autoland systems, you want multiple processors running independently to cross check results.

---

Real-time environments usually have "safety-critical" requirements. For that sort of thing, you could look at VxWorks, a popular real-time operating system. It's currently in use in many diverse arenas such as Boeing aircraft, BMW iDrive internals, RAID controllers, and various space craft. (Check it out.)

Development for the VxWorks platform can be done with several tools, among them Eclipse, Workbench, SCORE, and others. C, C++, Ada, and Fortran (yes, Fortran) are supported, as well as some others.

---

Since you don't give a platform, I would have to say C/C++. On most real-time platforms, you're relatively limited in options anyway.

The drawbacks of C's tendency to let you shoot yourself in the foot is offset by the number of tools to validate the code and the stability and direct mapping of the code to the hardware capabilities of the platform. Also, for anything critical, you will be unable to rely on third-party software which has not been extensively reviewed - this include most libraries - even many of those provided by hardware vendors.

Since everything will be your responsibility, you want a stable compiler, predictable behavior and a close mapping to the hardware.

---

Here's a few updates for some tools that I had not seen discussed yet that I've been playing with lately which are fairly good.

The LLVM Compiler Infrastructure, a short blurb on their main page (includes front-ends for C and C++. Front-ends for Java, Scheme, and other languages are in development);

A compiler infrastructure - LLVM is also a collection of source code that implements the language and compilation strategy. The primary components of the LLVM infrastructure are a GCC-based C & C++ front-end, a link-time optimization framework with a growing set of global and interprocedural analyses and transformations, static back-ends for the X86, X86-64, PowerPC 32/64, ARM, Thumb, IA-64, Alpha, SPARC, MIPS and CellSPU architectures, a back-end which emits portable C code, and a Just-In-Time compiler for X86, X86-64, PowerPC 32/64 processors, and an emitter for MSIL.

VCC;

VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.

VCC uses the recently released Common Compiler Infrastructure.

Both of these tools, LLVM or VCC are designed to support multiple languages and architectures, I do think that their is a rise in coding by contract and other formal verification practices.

WPF (not the MS framework :), is a good place to start if you're trying to evaluate some of the recent research and tools in the program validation space.

WG23 is the primary resource however for fairly current and specific critical systems development language details. They cover everything from Ada, C, C++, Java, C#, Scripting, etc... and have at the very least a decent set of reference and guidance for direction to update information on language specific flaws and vulnerabilities.

---

There are a lot of good references at http://www.dwheeler.com ("high-assurance software").

For automotive stuff, see the MISRA C standard. C but you can't use more than two levels of pointers, and some other stuff like that.

adahome.com has good info on Ada. I liked this C++ to Ada tutorial: http://adahome.com/Ammo/cpp2ada.html

For hard real-time, Tom Hawkins has done some interesting Haskell stuff. See: ImProve (language incorporates an SMT solver to check verification conditions) and Atom (EDSL for hard realtime concurrent programming without using actual threads or tasks).

---

A language that imposes careful patterns may help, but you can impose careful patterns using any language, even assembler. Every assumption about every value needs code that tests the assumption. For example, always test divisor for zero before dividing.

The more you can trust reusable components, the easier the task, but reusable components are seldom certified for critical use and will not get you through regulatory safety processes. You should use a tiny OS kernel and then build tiny modules that are unit tested with random input. A language like Eiffel might help, but there is no silver bullet.

---

Any software product can pass the DO-178b certification process using any tool but the questions is how difficult would it be. If the compiler isn't certified you may need to demonstrate your code is traceable at the assembly level. So it is helpful that your compiler is certified. We used C on our projects but had to verify at the assembly level and use a code standard that included turning off the optimizer, limited stack usage, limited interrupt usage, transparent certifiable libraries, etc. ADA isn't pixie dust but it makes the PSAC plan look more achievable.

As applicatons get larger, assembly code becomes less viable choice. The ARM processor just invites C++, but if you ask companies like Kiel it their tool is certified, they will return with a "huh?" And don't forget that verificaton tools also need to be certified. Try verifying a LabView test program.

---

A new safety-critical standard for Java is currently in development - JSR 302: Safety Critical Java Technology.

The Safety-Critical Java (SCJ) is based on a subset of RTSJ. The goal is to have a framework suitable for the development and analysis of safety critical programs for safety critical certification (DO-178B, Level A and other safety-critical standards).

SCJ for example removes the heap, which is still present in RTSJ, it also defines 3 compliance levels to which both application and VM implementation may conform, the compliance levels are defined to ease certification of variously complex applications.

Resources:

• Java for Safety-Critical Applications.
• JSR 302: Safety Critical Java Technology
• Developing Safety-Critical Applications with Java

---

I don't know what language I'd use, but I do know what language I wouldn't:

NOTE ON JAVA SUPPORT. THE SOFTWARE PRODUCT MAY CONTAIN SUPPORT FOR PROGRAMS WRITTEN IN JAVA. JAVA TECHNOLOGY IS NOT FAULT TOLERANT AND IS NOT DESIGNED, MANUFACTURED, OR INTENDED FOR USE OR RESALE AS ON-LINE CONTROL EQUIPMENT IN HAZARDOUS ENVIRONMENTS REQUIRING FAIL-SAFE PERFORMANCE, SUCH AS IN THE OPERATION OF NUCLEAR FACILITIES, AIRCRAFT NAVIGATION OR COMMUNICATION SYSTEMS, AIR TRAFFIC CONTROL, DIRECT LIFE SUPPORT MACHINES, OR WEAPONS SYSTEMS, IN WHICH THE FAILURE OF JAVA TECHNOLOGY COULD LEAD DIRECTLY TO DEATH, PERSONAL INJURY, OR SEVERE PHYSICAL OR ENVIRONMENTAL DAMAGE.

---

HAL/S is used for the Space Shuttle.

참고URL : https://stackoverflow.com/questions/243387/which-languages-are-used-for-safety-critical-software