論文の概要: Verifying User Interfaces using SPARK Ada: A Case Study of the T34 Syringe Driver

• arxiv url: http://arxiv.org/abs/2509.16681v1
• Date: Sat, 20 Sep 2025 13:14:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 15:04:51.910419
• Title: Verifying User Interfaces using SPARK Ada: A Case Study of the T34 Syringe Driver
• Title（参考訳）: SPARK Adaを用いたユーザインタフェースの検証:T34シリンジドライバを事例として
• Authors: Peterson Jean,
• Abstract要約: 多くのヒューマンファクターリスクは、実際の環境で適切なテストが完了するまでキャッチされない。 本研究は、T34シリンジドライバの動作モデルに対して、SPARK Adaの正式な検証ツールを使用する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The increase in safety and critical systems improved Healthcare. Due to their risk of harm, such systems are subject to stringent guidelines and compliances. These safety measures ensure a seamless experience and mitigate the risk to end-users. Institutions like the Food and Drug Administration and the NHS, respectively, established international standards and competency frameworks to ensure industry compliance with these safety concerns. Medical device manufacturing is mainly concerned with standards. Consequently, these standards now advocate for better human factors considered in user interaction for medical devices. This forces manufacturers to rely on heavy testing and review to cover many of these factors during development. Sadly, many human factor risks will not be caught until proper testing in real life, which might be catastrophic in the case of an ambulatory device like the T34 syringe pump. Therefore, effort in formal methods research may propose new solutions in anticipating these errors in the early stages of development or even reducing their occurrence based on the use of standard generic model. These generically developed models will provide a common framework for safety integration in industry and may potentially be proven using formal verification mathematical proofs. This research uses SPARK Ada's formal verification tool against a behavioural model of the T34 syringe driver. A Generic Infusion Pump model refinement is explored and implemented in SPARK Ada. As a subset of the Ada language, the verification level of the end prototype is evaluated using SPARK. Exploring potential limitations defines the proposed model's implementation liability when considering abstraction and components of User Interface design in SPARK Ada.
• Abstract（参考訳）: 安全と臨界システムの増大はヘルスケアを改善した。 危害のリスクがあるため、こうしたシステムは厳格なガイドラインとコンプライアンスの対象となっている。 これらの安全対策により、シームレスなエクスペリエンスが保証され、エンドユーザのリスクを軽減します。 食品医薬品局(FDA)やNHS(NHS)などの機関は、これらの安全上の懸念に業界が準拠することを保証するための国際標準と能力の枠組みを確立した。 医療機器の製造は主に標準に関するものである。 その結果、これらの標準は、医療機器のユーザーインタラクションにおいて考慮されたより良いヒューマンファクターを提唱している。 これにより、メーカーは、開発中にこれらの要素の多くをカバーするために、重いテストとレビューを頼らざるを得ない。 残念なことに、T34シリンジポンプのような膨らみのある装置の場合、現実の環境で適切なテストが完了するまで、多くのヒューマンファクターリスクはキャッチされないだろう。 したがって、形式的手法の研究における取り組みは、開発初期段階のエラーを予測したり、あるいは標準ジェネリックモデルを用いてそれらの発生を減らしたりするための新しい解決策を提案することができる。 これらの汎用的に開発されたモデルは、業界における安全統合のための共通のフレームワークを提供し、形式的な検証数学的証明を用いて証明される可能性がある。 本研究は、T34シリンジドライバの動作モデルに対して、SPARK Adaの正式な検証ツールを使用する。 SPARK Adaにおいて, ジェネリック・インフュージョン・ポンプ・モデルの改良を検討, 実施した。 Ada言語のサブセットとして、プロトタイプの検証レベルをSPARKを用いて評価する。 潜在的な制限の探索は、SPARK Adaにおけるユーザーインターフェイス設計の抽象化とコンポーネントを検討する際に提案されたモデルの実装責任を定義します。

関連論文リスト

• Steering Externalities: Benign Activation Steering Unintentionally Increases Jailbreak Risk for Large Language Models [62.16655896700062]
  活性化ステアリングは大規模言語モデル(LLM)の有用性を高める技術である 重要かつ過度に調査された安全リスクを無意識に導入することを示します。 実験によると、これらの介入は強制乗算器として機能し、ジェイルブレイクに新たな脆弱性を発生させ、標準ベンチマークで攻撃成功率を80%以上向上させる。
  論文  参考訳（メタデータ） (2026-02-03T12:32:35Z)
• Health-ORSC-Bench: A Benchmark for Measuring Over-Refusal and Safety Completion in Health Context [82.32380418146656]
  Health-ORSC-Benchは、医療におけるtextbfOver-Refusalと textbfSafe Completionの品質を測定するために設計された最初の大規模ベンチマークである。 私たちのフレームワークは、人間の検証を備えた自動パイプラインを使用して、さまざまなレベルの意図の曖昧さでモデルをテストします。 Health-ORSC-Benchは、次世代の医療AIアシスタントを調整するための厳格な標準を提供する。
  論文  参考訳（メタデータ） (2026-01-25T01:28:52Z)
• The Forgotten Shield: Safety Grafting in Parameter-Space for Medical MLLMs [23.79442915729949]
  医療マルチモーダル大言語モデル(Medical MLLMs)は、専門的な医療タスクにおいて顕著な進歩を遂げている。 しかし、彼らの安全性の研究は遅れており、現実の展開に潜在的なリスクを生じさせている。 我々はまず,現在のSOTA医療MLLMの安全性を体系的にベンチマークする多次元評価フレームワークを構築した。
  論文  参考訳（メタデータ） (2025-12-05T06:52:06Z)
• Building a Foundational Guardrail for General Agentic Systems via Synthetic Data [76.18834864749606]
  LLMエージェントは、計画段階で介入するマルチステップタスクを計画できる。 既存のガードレールは主にポスト・エグゼクティブ(英語版)を運用しており、スケーリングが困難であり、計画レベルで制御可能な監督を行う余地がほとんどない。 我々は、良性軌道を合成し、カテゴリーラベル付きリスクを困難に注入し、自動報酬モデルを介して出力をフィルタリングする制御可能なエンジンであるAuraGenを紹介する。
  論文  参考訳（メタデータ） (2025-10-10T18:42:32Z)
• D-REX: A Benchmark for Detecting Deceptive Reasoning in Large Language Models [62.83226685925107]
  Deceptive Reasoning Exposure Suite (D-REX)は、モデルの内部推論プロセスと最終的な出力との相違を評価するために設計された、新しいデータセットである。 D-REXの各サンプルには、敵システムプロンプト、エンドユーザーのテストクエリ、モデルの一見無害な応答、そして重要なことに、モデルの内部チェーンが含まれている。 我々は、D-REXが既存のモデルと安全メカニズムに重大な課題をもたらすことを実証した。
  論文  参考訳（メタデータ） (2025-09-22T15:59:40Z)
• Conformal Object Detection by Sequential Risk Control [3.3274747298291216]
  我々は,任意のデータセットサイズに有効な統計的保証を備えた,ポストホックな予測不確実性定量化手法を開発した。 まず、コンフォーマルオブジェクト検出(COD)の問題を正式に定義する。 コンフォーマルリスク制御の統計的保証を2つのシーケンシャルタスクに拡張する,シークエンシャルコンフォーマルリスク制御(SeqCRC)を提案する。 本稿では,SeqCRCを異なるケースや認定要件に適用するのに適した,古い,新しい損失関数と予測セットを提案する。
  論文  参考訳（メタデータ） (2025-05-29T22:19:01Z)
• What Makes and Breaks Safety Fine-tuning? A Mechanistic Study [64.9691741899956]
  安全性の微調整は、大規模な言語モデル(LLM)を、安全なデプロイメントのための人間の好みに合わせるのに役立つ。 安全でない入力の健全な側面をキャプチャする合成データ生成フレームワークを設計する。 これを用いて,3つのよく知られた安全微調整手法について検討する。
  論文  参考訳（メタデータ） (2024-07-14T16:12:57Z)
• The Need for Guardrails with Large Language Models in Medical Safety-Critical Settings: An Artificial Intelligence Application in the Pharmacovigilance Ecosystem [0.6965384453064829]
  大規模言語モデル(LLM)は、特定の種類の知識処理を効果的にスケールする能力を備えた有用なツールである。 しかし、高リスクで安全に重要な領域への展開は、特に幻覚の問題など、ユニークな課題を生んでいる。 これは特に、不正確さが患者を傷つける可能性がある薬物の安全性のような設定に関係している。 我々は、特定の種類の幻覚と薬物安全性のエラーを軽減するために特別に設計されたガードレールのコンセプトスイートを開発し、実証した。
  論文  参考訳（メタデータ） (2024-07-01T19:52:41Z)
• Detectors for Safe and Reliable LLMs: Implementations, Uses, and Limitations [76.19419888353586]
  大規模言語モデル(LLM)は、不誠実なアウトプットからバイアスや有害な世代に至るまで、さまざまなリスクを受けやすい。 我々は,様々な害のラベルを提供するコンパクトで容易に構築できる分類モデルである,検出器のライブラリを作成し,展開する取り組みについて述べる。
  論文  参考訳（メタデータ） (2024-03-09T21:07:16Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。