なぜブランは3台ではなく4台のコンピュータを持っていたのか

エンジニアリングブログ なぜブランは3台ではなく4台のコンピュータを持っていたのか -- そしてリーン証明が追加するもの 日付: 2026年9月24日 · 更新日: 2026年9月29日 An-225がブランを運ぶ、1989年。写真: Vasiliy Koba, CC BY-SA 4.0, via Wikimedia Commons; グレースケールに変換、トーン調整、トリミング。このバージョン: CC BY-SA 4.0。 TL;DR ブランのフライトコンピュータは、同じプログラムを同期して実行する4台の同一のBiser-4マシンでした。比較スキームが故障したマシンをブロックし、設計は任意の2つの障害を乗り越える必要がありました（セクション1）。4という数字は、出力を比較するだけで故障チャネルが見つかる場合の2つの障害のコストです。これはビザンチン合意の3f + 1ではなく、異なる問題です（セクション2と3）。1つのプログラムのコピーは、そのバグを共有します：STS-1、ボーイング787のジェネレータコントローラ、アリアン501、QF72。業界は、不一致と検証を組み合わせて対応します（セクション4）。比較ステップのRustモデル（ここではVoterと呼ばれる）には、コードAeneasが生成したコードに対して、Lean 4で証明された5つの定理と2つの系があります（セクション5と6）。証明はフライトコードではなくVoterをカバーしています：誤ったコマンドに同意する4つのチャネルは、それを通過させます（セクション4と7）。ここで使用されている証明ツールはDO-330認定を受けておらず、2026年9月の検索では、Rustツールチェーンの完了したDO-178CまたはECSS認定の公開記録は見つかりませんでした（セクション7と8）。 1988年11月15日、ソビエトのオービターブランはバイコヌールから打ち上げられ、初のそして唯一の飛行、無人のテスト飛行を行い、自動モードで着陸しました。その onboard コンピューティングは、NIIAP（現在はNPCAP）で設計されたBiser-4コンピュータから構築されたマルチチャネル複合体でした。4台の同一のBiser-4マシンが飛行しました。それぞれが冗長セットの1つのチャネルであり、ここからチャネルと呼びます。私がソースに飛び込んだきっかけは、それら4つのチャネルの説明の1つでした：同一のマシン、同期、同じプログラムを実行、出力での比較スキーム、そして任意の2つの障害を乗り越えるという要件。投票システムの教科書は3チャネルから始まります。そして、今日「4台のコンピュータ」と聞くエンジニアは、ビザンチン将軍の論文からのバウンドである3f + 1に手を伸ばしがちです。なぜなら、4は1つの障害に対する3f + 1だからです。ブランにとって、その読み方は間違っており、それが間違っている理由は、物語の最も有用な部分です。開示として、記事の後半は私の自身の仕事です。私はRustコードに関する機械チェック済みの証明を書いています。例えば、パニックしないことなどです。Leanで定理がチェックされたCOSEエンベロープパーサー cose-parse-nopanic はその1つです。Voterは小さく、冗長システムが発行するすべてのコマンドはそれを通過するため、同じパイプラインのテストとして適していました。セクション4が示すように、それに関する証明は、4つのチャネルが共有するバグについても何も語っておらず、その限界がその後のすべてを形作っています。セクション5より前のソースの読み込みは、その作業とは独立しています。 1. ソースがBiser-4、ブランの冗長フライトコンピュータについて述べていること Biser-4に関する公開記録は薄く、そのソースの重みは同じではありません。 1.1 重みの異なる4つのソース ほとんどの技術的な詳細は、Vadim Lukashevichの歴史サイトであるburan.ruから来ています。その制御システムページは、コンピューティング複合体、比較スキーム、同期について説明しており、単語幅やリンク速度までの特性表が含まれています。それらは著者名を記載しておらず、引用していない1995年の本に基づいているようです。この本は本記事ではチェックされていません。ブランのコンピューティングシステムの完全な開発を担当したPilyugin組織のV. D. Parondzhanovは、参加者のアカウントを残しています。これは2011年にRSDNフォーラムで再投稿されたものから知られています。どこで最初に現れたかは確立されていません。それは、飛行したマシンと、障害後の生存性のためにプログラムが書かれたことを追加します。NPCAPのB. N. VikhorevとA. G. Glazkovは、2007年の宇宙航行学に関するXXXI学術講演の要約（アーカイブコピー）で発表しました。これは開発者自身の見解です。Biser-4についてはほとんど述べていません。冗長性が4倍であったこと、そしてその理由についてです。詳細が示されているメカニズムは、前身に属しており、以下で区別されています。Keldysh応用数学研究所のV. KryukovとA. Petrenkoは、1996年の論文で、ブランの onboard システムソフトウェアのために作成された言語PROL2について説明しています。以下のロシア語の引用は翻訳されています。 1.2 述べられていることと、述べられていないこと 表は、ソースが述べていることと、それらのどれも述べていないことを並べています。後半は推論で埋めるべきギャップのリストではなく、私のモデルが独自のルールで補う必要があるもので、それぞれがセクション5でラベル付けされています。 質問 | ソースが述べていること | 出典、開発者 ---|---|--- Biser-4とは | NIIAP（Pilyugin）、現NPCAP | NPCAP; buran.ru 構成 | 2つの同一システム、中央と周辺、それぞれ4台のマシン | buran.ru 何が飛んだか | 中央システムのみ。周辺システムの空きスロットは、ブランキングプレートで閉じられていた | Parondzhanov プログラム | 同期、「同一のプログラムで」 | buran.ru; Parondzhanov 出力チェック | 各マシンの出力にある比較スキームが、4台すべてのコマンドを監視し、故障したマシンの出力はブロックされ、システムは3チャネル、次に2チャネルで継続する | buran.ru 要件 | 「任意の2つの障害下で」運用を維持すること。NPCAP: 「任意のパスで2つの障害要件を無条件に満たす」ための4重冗長性 | buran.ru; Vikhorev–Glazkov 同期 | ハードウェア。ソフトウェア同期は「極めて複雑で信頼性が低い」 | buran.ru; Parondzhanov チャネル間リンク | 毎秒61,440ワード（36ビット）。目的は不明 | buran.ru 障害発生後 | 1台、2台、3台の障害発生後の生存性のために、PPN（信頼性向上プログラム）が提供された | Parondzhanov 故障チャネルの特定方法 | 不明。buran.ruは単に「ブロックされた」と述べている。二次的なHabr記事：他の3台から「逸脱した」チャネルが切断された | Habr（二次的） 単一コマンドはどこで形成されるか | 不明。周辺ユニットがブロックされていない出力をどのように扱ったかは記述されていない | buran.ru 最後の2台が意見の相違をした場合どうなるか | 不明 | -- 入力は4台のマシンにどのように到達するか | 不明。周辺ユニットへの「ラジアル」リンクとチャネル間リンクのみが記述されている | buran.ru 非類似のバックアッププログラム | 不明。言及なし。不在の証拠ではなく沈黙 | -- PPNは何をしたか。ハードウェアとPPNの区別はどこか | 不明。PPNが提供されたことは述べられているが、そのメカニズムは不明 | -- 述べられている部分はアーキテクチャです。不明な部分は、冗長マネージャーの設計者が最初に尋ねる質問のリストです -- 故障チャネルがどのように特定されるか、意見の相違するペアがどうなるか、すべてのチャネルが同じ入力を見るか、4つの出力が1つのコマンドにどうなるか -- そしてそれらのすべてがBiser-4について未解決です。 1.3 要件とクロック Parondzhanovは、2つの障害要件が何のためであったかを述べています。任意の2つの障害下で、制御システムは「乗組員の命を救い、ブランを地球に帰還させる」ことを確保する必要がありました。buran.ruはそれをコンピューティング複合体に対する条件として述べており、NPCAPの要約は4重冗長性をそれに結びつけています。同期はハードウェアで行われました。buran.ruは理由を説明しています。リアルタイムで4台のマシンをソフトウェアで同期することは、許容される障害の任意の組み合わせの下では、「極めて複雑で信頼性が低い」からです。Parondzhanovは直接対比を引いています。「アメリカ人とは異なり、彼らはソフトウェア同期を使用した」のに対し、ブランの4台はハードウェアで同期されました。1つのクロックソースが、8台すべてのマシンに4 MHzのグリッドと32.8 msごとの割り込みを供給し、それ自体が5つの冗長チャネルとして構築され、各出力で3台のうち5台の投票を行いました。同期はここで重要です。なぜなら、単語ごとに、または単語ごとに、出力を比較することは、チャネルが同じフレームを同じ時間に計算している場合にのみ意味があるからです。1ステップ遅れているチャネルは、故障したチャネルとまったく同じように見えます。 1.4 1つのプログラム、そしてそれがどこにあったか 4台すべてのチャネルは同じプログラムを実行していました。buran.ruとParondzhanovは同じ言葉でそれを述べています。buran.ruのソフトウェアページは、それらがどのように...