論文の概要: Translating a VDM Model of a Medical Device into Kapture

• arxiv url: http://arxiv.org/abs/2506.09636v1
• Date: Wed, 11 Jun 2025 11:50:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-13 06:35:02.902092
• Title: Translating a VDM Model of a Medical Device into Kapture
• Title（参考訳）: 医療機器のVDMモデルへの変換
• Authors: Joe Hare, Leo Freitas, Ken Pierce,
• Abstract要約: 本稿では、D-RisQによって開発された公式なモデリングツールであるKaptureを用いて、既存の医療インプラントの形式的なVDMモデルを翻訳する。 本稿は,Kaptureのユーザビリティ,形式モデリングの課題,翻訳モデルの有効性を評価する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As the complexity of safety-critical medical devices increases, so does the need for clear, verifiable, software requirements. This paper explores the use of Kapture, a formal modelling tool developed by D-RisQ, to translate an existing formal VDM model of a medical implant for treating focal epilepsy called CANDO. The work was undertaken without prior experience in formal methods. The paper assess Kapture's usability, the challenges of formal modelling, and the effectiveness of the translated model. The result is a model in Kapture which covers over 90% of the original VDM model, and produces matching traces of results. While several issues were encountered during design and implementation, mainly due to the initial learning curve, this paper demonstrates that complex systems can be effectively modelled in Kapture by inexperienced users and highlights some difficulties in translating VDM specifications to Kapture.
• Abstract（参考訳）: 安全クリティカルな医療機器の複雑さが増大するにつれて、明確で検証可能なソフトウェア要件も必要になる。 本稿では、D-RisQによって開発された公式なモデリングツールであるKaptureを用いて、CANDOと呼ばれる局所てんかん治療のための医療インプラントの形式的VDMモデルを翻訳する。 形式的な手法で事前の経験のない作業が行われた。 本稿は,Kaptureのユーザビリティ,形式モデリングの課題,翻訳モデルの有効性を評価する。 その結果はKaptureのモデルであり、元のVDMモデルの90%以上をカバーし、一致した結果のトレースを生成する。 設計と実装においていくつかの問題が発生したが、主に学習曲線が原因であり、未経験者によって複雑なシステムをKaptureで効果的にモデル化できることを示し、VDM仕様をKaptureに翻訳することの難しさを強調した。

関連論文リスト

• Tomographic Foundation Model -- FORCE: Flow-Oriented Reconstruction Conditioning Engine [9.228750443979733]
  深層学習はCT画像再構成を著しく進歩させた。 ディープラーニングの手法は、ほぼペアのデータでうまく機能するが、それらは本質的に幻覚のリスクを負う。 我々は新しいCTフレームワークFORCE(Flow-Oriented Restruction Conditioning Engine)を提案する。
  論文  参考訳（メタデータ） (2025-06-02T18:25:12Z)
• CoMT: Chain-of-Medical-Thought Reduces Hallucination in Medical Report Generation [20.59298361626719]
  医療報告生成における幻覚を緩和するためのチェーン・オブ・メディカル・シント・アプローチ(CoMT)を提案する。 CoMTは、診断手順を分解することで、人間の医師の認知過程を模倣しようとしている。
  論文  参考訳（メタデータ） (2024-06-17T12:03:32Z)
• Medical Vision-Language Pre-Training for Brain Abnormalities [96.1408455065347]
  本稿では,PubMedなどの公共リソースから,医用画像・テキスト・アライメントデータを自動的に収集する方法を示す。 特に,まず大きな脳画像テキストデータセットを収集することにより,事前学習プロセスの合理化を図るパイプラインを提案する。 また,医療領域におけるサブフィギュアをサブキャプションにマッピングするというユニークな課題についても検討した。
  論文  参考訳（メタデータ） (2024-04-27T05:03:42Z)
• Towards a clinically accessible radiology foundation model: open-access and lightweight, with automated evaluation [113.5002649181103]
  オープンソースの小型マルチモーダルモデル(SMM)を訓練し、放射線学における未測定臨床ニーズに対する能力ギャップを埋める。 トレーニングのために,697万以上の画像テキストペアからなる大規模なデータセットを組み立てる。 評価のために,GPT-4に基づく実測値CheXpromptを提案する。 LlaVA-Radの推論は高速で、単一のV100 GPU上でプライベート設定で実行できる。
  論文  参考訳（メタデータ） (2024-03-12T18:12:02Z)
• Intensive Care as One Big Sequence Modeling Problem [1.6114012813668932]
  本稿では、患者と医療提供者とのインタラクションをイベントストリームとして表現する、シーケンスモデリングとしてのヘルスケアのパラダイムを提案する。 我々はMIMIC-IVデータセットから一様イベントストリームフォーマットに異種臨床記録を変換したシーケンスモデリングベンチマークMIMIC-SEQを開発した。
  論文  参考訳（メタデータ） (2024-02-27T13:36:55Z)
• Large Language Model Distilling Medication Recommendation Model [58.94186280631342]
  大規模言語モデル(LLM)の強力な意味理解と入力非依存特性を利用する。 本研究は, LLMを用いて既存の薬剤推奨手法を変換することを目的としている。 これを軽減するため,LLMの習熟度をよりコンパクトなモデルに伝達する機能レベルの知識蒸留技術を開発した。
  論文  参考訳（メタデータ） (2024-02-05T08:25:22Z)
• Customizing General-Purpose Foundation Models for Medical Report Generation [64.31265734687182]
  ラベル付き医用画像-レポートペアの不足は、ディープニューラルネットワークや大規模ニューラルネットワークの開発において大きな課題となっている。 本稿では,コンピュータビジョンと自然言語処理の基盤モデル (FM) として,市販の汎用大規模事前学習モデルのカスタマイズを提案する。
  論文  参考訳（メタデータ） (2023-06-09T03:02:36Z)

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

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