文章基本信息

标题：複数事象の発生を含意した区間振る舞い記述法とその検証法の提案
本地全文：下载
作者：張漢明 ; 野呂昌満 ; 沢田篤史等
期刊名称：コンピュータソフトウェア
印刷版ISSN：0289-6540
出版年度：2017
卷号：34
期号：2
页码：2_3-2_15
DOI：10.11309/jssst.34.2_3
出版社：Japan Society for Software Science and Technology
摘要：並行システム開発において，特に組み込みシステムでは並列に動作する複数のハードウェア装置のもとで複数の事象が並列に発生するので，同時に発生する事象を考慮する必要がある．我々はCSPに代表されるプロセス代数を用いて，同時の事象を含んだ振る舞いを形式的に記述して分析する方法を提案する．プロセス計算ではプロセスは事象の列としてモデル化されるので，同時の事象は複雑な記述になる．本稿では，複数事象の同時性の概念を明確にしCSPを用いてその記述法と検証法を提示する．自動販売機制御の事例を用いて提案する記述方法の有用性について議論する．