「形式手法」の記事一覧

• Dezyneで構築する検証可能な並行制御ソフトウェア

  2025-05-17 09:44

  科学・技術

  Dezyneは、並行制御ソフトウェアを形式的に設計・検証・実装するためのプログラミング言語およびツール群です。状態遷移やメッセージパッシングに基づき、デッドロックや非決定性のないモデルを保証しつつ、構造と動作を統一的に記述可能です。特にサイバーフィジカルシステムや組込み分野に適しており、構成要素間の契約設計によって複雑性の管理を容易にします。オープンソースで提供されています。

• TLA+ツール開発の現状と課題

  2025-05-15 18:53

  科学・技術

  2025年のTLA+コミュニティイベントでは、ツール開発の現状と今後の展望が議論されました。主要パーサやモデルチェッカーは複数存在し、多様な用途に対応していますが、コードのレガシー性と知識継承の課題が指摘されています。開発者の知識が断絶しがちな状況を克服するため、テストの充実、開発者オンボーディング、資金提供の3つが重要とされ、今後の発展にはコミュニティの連携と支援が不可欠とされています。