在系統發展中，時間因素是開發人員相當注重的特性之一，特別是在今天有著越來越多的即時性系統充斥在我們的生活之中，為此，在UML 2.0中，OMG(Object Management Group)新增了時間圖(Timing Diagram)此一新圖形，讓開發人員能針對時間做進一步的描述，但UML為一塑模工具(Modeling language)，並沒有提供進行分析驗證的相關方法，因此，開發人員在使用時間圖塑模時難以察覺其中隱含的錯誤。在驗證方面，派翠網路(Petri Net)相關的各項技術由於多年來有不少學者研究出針對各種不同的領域的驗證技術，已有些學者的研究是利用UML之塑模後模型配合派翠網路之各項特性以進行分析。在本論文的著重點為UML 2.0新增之時間圖，為此，我們提出一轉換時間圖至物件導向時間派翠網路(Object-Oriented Petri Nets)之機制，包含對時間圖、物件導向時間派翠網路之正規化規格及轉換規則，再轉換後利用派翠網路之各種分析能力對時間特性進行分析驗證，在本論文使用之範例為一簡單的行動通訊裝置與基地台之互動，經時間圖轉換至物件導向時間派翠網路後進行可達性分析(Reachability Analysis)，以驗證需求規格制定是否正確。 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.
