論文の概要: WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
- arxiv url: http://arxiv.org/abs/2407.21152v2
- Date: Sun, 18 Aug 2024 22:29:13 GMT
- ステータス: 処理完了
- システム内更新日: 2024-08-21 01:49:20.500210
- Title: WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+
- Title（参考訳）: WIP: TLA+を使ったソフトウエアエンジニアリングにおけるモデルチェックのための大学院生の紹介
- Authors: Konstantin Läufer, Gunda Mertin, George K. Thiruvathukal,
- Abstract要約: 我々は,コンピュータサイエンスプログラムにおける形式的手法の状態を質的に評価することを目的としている。
卒前研究の中間に含めることができるレベル適合例を構築した。
- 参考スコア（独自算出の注目度）: 0.358439716487063
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Background: In this paper, we present our initial efforts to integrate formal methods, with a focus on model-checking specifications written in Temporal Logic of Actions (TLA+), into computer science education, targeting undergraduate juniors/seniors and graduate students. Formal methods can play a key role in ensuring correct behavior of safety-critical systems, yet remain underutilized in educational and industry contexts. Aims: We aim to (1) qualitatively assess the state of formal methods in computer science programs, (2) construct level-appropriate examples that could be included midway into one's undergraduate studies, (3) demonstrate how to address successive "failures" through progressively stringent safety and liveness requirements, and (4) establish an ongoing framework for assessing interest and relevance among students. Methods: After starting with a refresher on mathematical logic, students specify the rules of simple puzzles in TLA+ and use its included model checker (known as TLC) to find a solution. We gradually escalate to more complex, dynamic, event-driven systems, such as the control logic of a microwave oven, where students will study safety and liveness requirements. We subsequently discuss explicit concurrency, along with thread safety and deadlock avoidance, by modeling bounded counters and buffers. Results: Our initial findings suggest that through careful curricular design and choice of examples and tools, it is possible to inspire and cultivate a new generation of software engineers proficient in formal methods. Conclusions: Our initial efforts suggest that 84% of our students had a positive experience in our formal methods course. Future plans include a longitudinal analysis within our own institution and proposals to partner with other institutions to explore the effectiveness of our open-source and open-access modules.
- Abstract（参考訳）: 背景: 本稿では, 時間的行動論理(TLA+)で記述されたモデルチェック仕様を, 大学生や大学院生を対象にしたコンピュータサイエンス教育に取り入れることを目的とした, フォーマルな手法の統合に向けた最初の取り組みについて述べる。
形式的手法は、安全クリティカルなシステムの正しい行動を保証する上で重要な役割を果たすが、教育や産業の文脈では未利用のままである。
目的:(1)コンピュータサイエンスプログラムにおける形式的手法の実態を質的に評価すること,(2)学部生の学習の途中で含めることができるレベル適合例の構築,(3)段階的に厳格な安全性と生活性の要件を通じて連続した「障害」に対処する方法の実証,(4)学生の関心と関連性を評価するための継続的な枠組みを確立することを目指す。
方法: 数学的論理学のリフレッシュから始めると、生徒はTLA+の単純なパズルのルールを指定し、その内包されたモデルチェッカー(TLC)を使って解を見つける。
マイクロ波オーブンの制御ロジックなど、より複雑でダイナミックなイベント駆動システムに徐々にエスカレートし、学生は安全と生活性の要件を学習する。
その後、境界カウンタとバッファをモデル化することにより、スレッド安全性とデッドロック回避とともに、明示的な並行性について議論する。
結果: 初期の知見から, 慎重に設計し, 実例やツールの選択を行うことで, 新世代のソフトウェアエンジニアが形式的な手法で熟達し, 育成できることが示唆された。
結論:最初の取り組みは,学生の84%が形式的方法のコースで肯定的な経験をしていたことを示唆した。
今後の計画には、当社の機関内での縦断的な分析や、他の機関とパートナーシップを結び、当社のオープンソースおよびオープンアクセスモジュールの有効性を探求する提案が含まれます。
関連論文リスト
- SMLE: Safe Machine Learning via Embedded Overapproximation [4.129133569151574]
本研究は,デザイナ・ちょうせん特性を満たすことが保証される識別可能なMLモデルを訓練する作業について考察する。
現代のニューラルモデルにおけるコンプライアンスの厳格な検証と実施という計算複雑性のため、これは非常に難しい。
1)保守的なセマンティクスによる効率的な検証を可能にする汎用的,シンプルなアーキテクチャ。
回帰における線形不等式によって定義される特性と、多重ラベル分類における相互排他的クラスに対するアプローチを評価する。
論文 参考訳（メタデータ） (2024-09-30T17:19:57Z) - Scalable Language Model with Generalized Continual Learning [58.700439919096155]
The Joint Adaptive Re-ization (JARe) is integrated with Dynamic Task-related Knowledge Retrieval (DTKR) to enable adapt adjust of language model based on specific downstream task。
提案手法は,様々なバックボーンやベンチマーク上での最先端性能を実証し,最小限の忘れを伴い,フルセットおよび少数ショットのシナリオにおいて効果的な連続学習を実現する。
論文 参考訳（メタデータ） (2024-04-11T04:22:15Z) - Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
機械学習(ML)をサイバー物理システム(CPS)に統合することは大きな利益をもたらす。
既存の検証と検証技術は、しばしばこれらの新しいパラダイムには不十分である。
本稿では, 基礎確率テストからより厳密なアプローチへ移行し, 正式な保証を実現するためのロードマップを提案する。
論文 参考訳（メタデータ） (2023-11-13T14:56:14Z) - Large Language Models for In-Context Student Modeling: Synthesizing Student's Behavior in Visual Programming [29.65988680948297]
本研究では,大規模言語モデル(LLM)のオープンエンド学習領域におけるコンテキスト内学習モデルへの応用について検討する。
学生の行動に LLM を利用する新しいフレームワーク LLM for Student Synthesis (LLM-SS) を導入する。
LLM-SSフレームワークに基づいて複数の手法をインスタンス化し、既存のベンチマークであるStudioSynを用いて視覚的プログラミング領域における学生の試行合成を行う。
論文 参考訳（メタデータ） (2023-10-15T12:56:13Z) - CoopInit: Initializing Generative Adversarial Networks via Cooperative
Learning [50.90384817689249]
CoopInitは、協力的な学習ベースの戦略で、GANにとって良い出発点を素早く学べる。
本稿では,画像生成における提案手法の有効性を示す。
論文 参考訳（メタデータ） (2023-03-21T07:49:32Z) - Learning to Generate All Feasible Actions [4.333208181196761]
アクションマッピングは、学習プロセスを2つのステップに分割する新しいアプローチである。
本稿では、実現可能性モデルの自己教師型クエリにより、実現可能なすべてのアクションを生成することを学ぶことで、実現可能性部分に焦点を当てる。
エージェントが接続不能な実行可能なアクションセット間でアクションを生成する能力を示す。
論文 参考訳（メタデータ） (2023-01-26T23:15:51Z) - Evaluating Model-free Reinforcement Learning toward Safety-critical
Tasks [70.76757529955577]
本稿では、国家安全RLの観点から、この領域における先行研究を再考する。
安全最適化と安全予測を組み合わせた共同手法であるUnrolling Safety Layer (USL)を提案する。
この領域のさらなる研究を容易にするため、我々は関連するアルゴリズムを統一パイプラインで再現し、SafeRL-Kitに組み込む。
論文 参考訳（メタデータ） (2022-12-12T06:30:17Z) - Learning Multi-Objective Curricula for Deep Reinforcement Learning [55.27879754113767]
深部強化学習(DRL)のサンプル効率と最終性能を向上させるために,各種自動カリキュラム学習(ACL)手法が提案されている。
本稿では,多目的だがコヒーレントなカリキュラムを作成するための統合された自動カリキュラム学習フレームワークを提案する。
既存の手設計のカリキュラムパラダイムに加えて,抽象カリキュラムを学習するためのフレキシブルなメモリ機構を設計する。
論文 参考訳（メタデータ） (2021-10-06T19:30:25Z) - Evaluating the Safety of Deep Reinforcement Learning Models using
Semi-Formal Verification [81.32981236437395]
本稿では,区間分析に基づく半形式的意思決定手法を提案する。
本手法は, 標準ベンチマークに比較して, 形式検証に対して比較結果を得る。
提案手法は, 意思決定モデルにおける安全性特性を効果的に評価することを可能にする。
論文 参考訳（メタデータ） (2020-10-19T11:18:06Z) - BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration [72.88493072196094]
プログラムのボトムアップ検索に学習を活用する新しい合成手法を提案する。
特に、入力出力例のセットに基づいて、探索条件中の中間値の合成を優先順位付けするようにモデルを訓練する。
単純な教師付き学習アプローチであっても,学習とボトムアップ検索の組み合わせは極めて効果的であることを示す。
論文 参考訳（メタデータ） (2020-07-28T17:46:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。