論文の概要: 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におけるユーザーインターフェイス設計の抽象化とコンポーネントを検討する際に提案されたモデルの実装責任を定義します。

関連論文リスト

• 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)

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

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