Paper Info
Title
Qualitative verification of finite and real-time DEVS networks
Abstract
This paper introduces a qualitative verification methodology for a subclass of RTDEVS(Real-Time Discrete Event System Specification) [4], called Finite RTDEVS(FRTDEVS). Sub-classing FRTDEVS from RTDEVS aims to generate a finite structure of reachability graph for a given network of FRTDEVS. Since the reachability graph is isomorphic to a given FRTDEVS network in terms of their behaviors, it enables us to verify some qualitative properties of the target system. In order to demonstrate a practical usage of the reachability graph, we illustrate how to check safety and liveness monorail systems modeled by FRTDEVS networks.
Year
Venue
Keywords
2012
SpringSim (TMS-DEVS)
qualitative verification methodology,sub-classing frtdevs,real-time devs network,liveness monorail system,qualitative property,frtdevs network,reachability graph,real-time discrete event system,finite structure,practical usage,finite rtdevs
Field
DocType
Volume
Graph,Computer science,Theoretical computer science,Reachability,Isomorphism,Monorail,DEVS,Liveness
Conference
44
Issue
ISSN
Citations 
4
0735-9276
3
PageRank 
References 
Authors
0.49
6
1
Name
Order
Citations
PageRank
Moon Ho Hwang1404.77