抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
同期的反応性データフローは,IoTシステムの局所同期成分を含む組込みおよびサイバー物理システムに対する高レベル抽象プログラミングモデルを提供するパラダイムである。そのようなシステムにおけるセキュリティは,低レベルプログラミング,不明確なインタフェイス,およびデータのセキュリティ分類への不注意のため,ひどく損なわれる。同期的反応性データフロー言語にDenning型格子ベースの安全な情報フローフレームワークを組み込むことによって,そのようなシステムのための正しいおよび安全な構成実装が特定され,導出されるフレームワークを提供する。特に,セキュリティ型システムによるLustreプログラミングフレームワークの拡張を提案した。タイプシステムの新規性は,セキュリティタイプ変数,特にノード呼び出しの処理における制約の記号的定式化にあり,セキュリティクラス格子に関する安全なフローに関する理由を可能にする。主な定理は,Lustreの共同誘導操作意味論に関して,著者らのタイプシステムの健全性であり,著者らは,よくタイプ化されたプログラムが,非干渉を示すことによって証明した。完全な言語に取り組むよりむしろ,著者らは,最初に,著者らのタイプシステムがはるかに単純である「正規化されたルストル」(Nlusterre)と呼ばれるよく行動されたサブ言語に対する非干渉結果を証明した。次に,著者らはBourke et al.の意味論保存「正規化」変換が,LustreからNLustreへの変換もセキュリティ保存であることを示した。正規化変換によるセキュリティ型のこの保存は,コンパイラ変換のレベルにおいて,「被験者削減」に対する特性である。良いセキュリティ型Lustreプログラムは,意味論保存(Bourke et al.)とタイプ保存結果によるNLstreに対する非干渉の以前の結果への低減から,非干渉である。【JST・京大機械翻訳】
