|
SP-DEVS abbreviating "Schedule-Preserving Discrete Event System Specification" is a formalism for modeling and analyzing discrete event systems in both simulation and verification ways. SP-DEVS also provides modular and hierarchical modeling features which have been inherited from the Classic DEVS. == History == SP-DEVS has been designed to support verification analysis of its networks by guaranting to obtain a finite-vertex reachability graph of the original networks, which had been an open problem of DEVS formalism for roughly 30 years. To get such a reachability graph of its networks, SP-DEVS has been imposed the three restrictions: # finiteness of event sets and state set, # the lifespan of a state can be scheduled by a rational number or infinity, and # preserving the internal schedule from any external events. Thus, SP-DEVS is a sub-class of both DEVS and FD-DEVS. These three restrictions lead that SP-DEVS class is closed under coupling even though the number of states are finite. This property enables a finite-vertex graph-based verification for some qualitative properties and quantitative property, even with SP-DEVS coupled models. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「SP-DEVS」の詳細全文を読む スポンサード リンク
|