%0 Journal Article
%T Model Checking of Timed Petri Nets to Semantically Equivalent Timed Automata Based on Uppaal<br>基于Uppaal的时延Petri网到时间自动机等价模型验证
%A ZHOU Qing-lei
%A WANG Jing
%A <br>周清雷
%A 王静
%J 计算机应用研究
%D 2005
%I 
%X Both timed Petri nets and timed automata can carry on behavior simulation and performance analysis to the real-time system effectively.Utilizes a translation algorithm (referred to as TPN-to-TA translation) which can map a timed Petri nets model of real-time system into a collect of semantically equivalent timed automata, use a mature model checker Uppaal for timed automata to verify the performance of this timed Petri nets model.
%K Timed Petri Nets
%K Timed Automata
%K TPN-to-TA Translation
%K Uppaal<br>时延Petri网
%K 时间自动机
%K TPN-to-TA转换
%K Uppaal
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=A37F94C1D8CB471F&yid=2DD7160C83D0ACED&vid=BC12EA701C895178&iid=B31275AF3241DB2D&sid=0401E2DB1F51F8DE&eid=5C3443B19473A746&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=9