（６１）並列プログラム開発支援システム：ＭＥＮＤＥＬＳ　ＺＯＮＥ

	マ シ ン：Multi-PSI
	環　　境：PIMOS, SIMPOS
	言　　語：ESP, KL1
	ソース量：10 MB
	文　　書：マニュアル (英語／日本語)

概要

特徴

機能

●オブジェクト生成：

等式論理によって記述されたオブジェクトの仕様が、項書換え技法によっ て並列に自動検証される。正しさの確認された仕様からは、オブジェクトのプ ログラムが自動生成される。

●オブジェクト結合：

高レベルペトリネットによって表現されたオブジェクトを、ユーザが結合 する。

●オブジェクト調整：

タイミングに関する制約を時相論理によって記述する。ペトリネットで表 されたオブジェクトがその仕様を満たさない場合は、定理証明手法により仕様 を満たすように自動的に調整される。

　┌─────────┐　　　　　┌───────┐
　│オブジェクトの仕様│────＞│　　　　　　　│
　└─────────┘　　　　　│　　　　　　　│
　┌───────────┐　　　│　　　　　　　│　　　┌────────┐
　│オブジェクトの結合情報│──＞│ＭＥＮＤＥＬＳ│──＞│ＫＬ１プログラム│
　└───────────┘　　　│　　ＺＯＮＥ　│　　　└────────┘
　┌─────────┐　　　　　│　　　　　　　│
　│タイミング制約　　│────＞│　　　　　　　│
　└─────────┘　　　　　└───────┘

参考文献

1. Honiden,S.,et al.: An Application of Structural Modeling and Automated Reasoning to Real-Time Systems Design, The Journal of Real-Time systems,Vol.1,No.3,pp.313-331(1990).

2. Ohsuga, A.,et al:Metis: A Term Rewriting System Generator,in Software Science and Engineering(Nakata,I.and Hagiya,M.eds.),pp.1-15,World Scientific(1991).

3. Uchihira,N.,et al.:Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic, Trans. IEICE,Vol.E73,No.12,pp.2001-2010(1990).

ＦＴＰ

• 並列プログラム開発支援システム：ＭＥＮＤＥＬＳ　ＺＯＮＥ [1,001K]