文献

J-GLOBAL ID：201802218162969816   整理番号：18A0848905

LTL ASSUME/保証契約のライブラリからの合成のための仕様分解【JST・京大機械翻訳】

Specification decomposition for synthesis from libraries of LTL Assume/Guarantee contracts

著者 (3件)： Iannopollo Antonio (EECS Department, University of California, Berkeley, Berkeley, USA) ,  Tripakis Stavros (EECS Department, University of California, Berkeley, Berkeley, USA) ,  Sangiovanni-Vincentelli Alberto (EECS Department, University of California, Berkeley, Berkeley, USA)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2018  号： DATE  ページ： 1574-1579  発行年： 2018年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 契約ベースの設計は複雑なシステムの組成設計を可能にする方法である。仕様を表現する契約を与えると,多くの単純な契約を構成することにより,それを形式的に満足することができる。これらの簡単な契約を既存のソリューションのライブラリから選択するとき,契約ライブラリからの合成について話す。合成過程を自動化する技術があるが,特に複雑な仕様に対して,それらは計算的に集中的である。本論文では,仕様を分割するための効率的な手法,すなわち,LTLベースのAssum/Guarante契約を,独立に満足できる多数のより簡単なサブ仕様において記述した。これらのすべての小さな問題が解決されると,元の仕様を満足させるためにそれらの解を安全に融合することが可能である。産業事例研究における本手法の有効性を示した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【JST・京大機械翻訳】

シソーラス用語： 自動化 ,  *事例研究 ,  安全性

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (5件)： 保証 ,  契約 ,  ライブラリ ,  仕様 ,  分解