文献

J-GLOBAL ID：201902269075935354   整理番号：19A0889228

OTS/CafeOBJ法によるマルチタスク実時間システムの仕様記述

Specification description and of real-time multitask systems by the OTS/CafeOBJ method

著者 (4件)： 東周輝 (富山県大) ,  中村正樹 (富山県大) ,  榊原一紀 (富山県大) ,  緒方和博 (北陸先端科学技術大学院大)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 118  号： 499(MSS2018 81-95)  ページ： 13-18  発行年： 2019年03月07日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本研究では,形式手法であるOTS/CafeOBJ法を用いて,マルチタスク実時間システムの仕様を記述し,検証する手法の構築を目指す.マルチタスク実時間システムでは各プロセスが並行動作するため,取り得る状態が膨大になり,時間制約が適切に与えられているかどうかの確認は容易ではない.マルチタスク実時間システムの形式仕様を記述することで,コンピュータ支援による時間制約の形式的な検証が可能となる.本発表では,複数プロセスが個々に時間制約を持つようなシステムをOTS/CafeOBJ仕様として形式的に記述する手法を提案する.(著者抄録)

シソーラス用語： システム ,  実時間処理 ,  *計算機処理方式 ,  多重処理 ,  *仕様記述 ,  制約条件 ,  *形式記述 ,  ソフトウェア工学
準シソーラス用語： マルチタスク ,  *形式仕様記述 ,  時間制約 ,  実時間システム

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

引用文献 (6件)：

• R. Diaconescu and K. Futatsugi, CafeOBJ Report, World Scientific, Singapore, 1998.
• 二木厚吉,緒方和博,中村正樹, ′′CafeOBJ入門(1)-(6),′′ コンピュータソフトウェア, 25(2) pp.1-27, 25(3) pp.69-80, 25(4) pp.68-84, 26(1) pp.71-83, 26(2) pp.93-106, 2008, 2009.
• K. Ogata, and K. Futatsugi, ′′Proof scores in the OTS/-CafeOBJ method,′′ In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.2884, pp.170âĂŞ184. Springer, Heidelberg,2003.
• K. Ogata and K. Futatsugi, ′′Some tips on writing proof scores in the OTS/CafeOBJ method,′′ In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift. LNCS, vol.4060, pp.596âĂŞ615. Springer, Heidelberg, 2006.
• 緒方和博, ′′代数仕様に基づく実時間システムの検証,′′ 計測と制御, 48(11): 816-821, 2009.

タイトルに関連する用語 (4件)： OTS ,  マルチタスク ,  実時間システム ,  仕様記述