臺灣博碩士論文加值系統

系統中的每一成員(component)分散管理, 又要使成員間彼此聯繫, 所以分散式環境中
的時間性更不易控制, 多媒體系統是多種媒體的組合運作, 但是每一種媒體的播放速度都
不盡相同, 所以為求得較佳的QoS, 各種媒體的同步是很種要的, 同步所
考慮的正式時間性.
雖然即時性的要求隨著分散式與多媒體時代的到來, 其重要性越來越迫
切. 驗證即時系統的
正確性是很困難的, 因為一個系統要考慮時間性質就會變得很困難, 近年
來的學者提出形式
方法來驗證一個系統的安全性, 然而形式方法的驗證過程的演算法, 其計算複雜肚腸常是
NP-Complete的問題, 常使電腦付出很大的代價, 驗證的過程過於複雜反而使系統的效率更
加惡化. 本研究的焦點是: 描是如何在兩種系統描述工具中, 增家時間性
的屬性及其與時間
有關的性質的驗證, 以及擴充時間性質的設計構想. 其中, 若使用Real-time Temporal
Logic 來作為系統的驗證工具, 其驗證的演算法可導入"經驗法則(
heuristics)"可減少驗證
過程所需計算的次數. 最後將使用PWP-heuristic這種可以驗證即時反應
的演算法來驗證Time
Petri Net安全性質.

Components in a distributed system are managed independently and yet, for
achieving common goals, need communicate and coordinate with each other.
System wide time-related properties are thus very hard to capture and manage.
In a multimedia application, media instances of different modes and speeds need
proper orchestration to accomplish joint tasks. The ovjectives of required
quality of service and synchronization are all time related properties. With
the age of distributed multimedia coming, the need to handle time related
properties, especially real time properties, can not be neglected.
However, correctness vertification is well recognized to be very difficult, not
to mention when real time properties are invlved. /formal methods were used to
verify temporal safeness; however, with inherent algorithmic complexity of NP-
completeness, these methods often overload computers with worse performance.
The study first focuses on how to add real time features to classical system
modeling tools, Petri net and temproal logic, after examining how notions of
time are present in systems. We then explain examples of verification of
temporal properties in these tools. Heuristics for a formal real time temporal
logic system, are then studied and practiced in an example to verify temporal
responsiveness of a timed Petri net.