Verifying Time Properties by Transforming Timing Diagram to Object-Oriented Time Petri Net

• Main Authors: Cain, 蔡祁名
• Other Authors: William C. Chu
• Format: Others
• Language: zh-TW
• Published: 2005
• Online Access: http://ndltd.ncl.edu.tw/handle/85513332010482606839

碩士 === 東海大學 === 資訊工程與科學系 === 93 === In system software development, time is a very important factor to the quality of the systems. Especailly there are more and more real time systems and embedded systems around people. Therefore, in UML 2.0 standard, OMG developed a new diagram called timing diagram which is used to described timing properties and interaction between objects. However, UML is a modeling language, it doesn't provide the technique to analyze and verify. For this reason, developers use timing diagram to describe the time properties but hard to know if there has some mistakes in timing diagram. The techniques of Petri nets are researched for years, and there are various analysis techniques to different domain. Some scholars’ research is to analyze the UML model by Petri net's analyzing properties. The focus of this thesis is on timing diagram. For this reason, we propose a mechanism to transform timing diagram to object-oriented time Petri net, it includes the specification of the timing diagram, the specification of the object-oriented time Petri net, and the transformation rules. After transforming, we utilize the analyzing abilities of Petri net to verify the timing properties. The example of this thesis is use the reachability analysis of Petri net to verify the correctness of the requirement.