Real-time system specification and analysis using Petri nets and temporal logics

The objective of this thesis is to provide a formal method for specifying and analyzing real-time systems from the "time" perspective. Thus, I present an extension of Petri nets called timing constraint Petri nets (TCPNs), and an extension of branching-time temporal logic called reachability graph logic (RGL) to realize this objective.;Many system behavioral properties, such as liveness (deadlock-free) and fairness (starvation-free) can be modeled and analyzed with Petri nets. However, Petri nets alone cannot represent some of the temporal properties such as eventually. Thus RGL is needed in order to express and verify those system behavioral properties over a net structure. Therefore, the integration of TCPNs and RGL, in which TCPNs for specifications and timing analysis and RGL for temporal properties expression and reasoning is a proper combination for specifying and analyzing real-time systems.;TCPNs are derived from the concepts of timing constraints and Petri nets. TCPNs extend Petri nets by associating timing constraints with transitions and places. Based on TCPNs, this thesis presents a schedulability analysis which is performed during the specification phase to verify a system specification against its imposed timing constraints. The analysis method presented in this paper can be used regardless of scheduling algorithms. RGL is a branching-time propositional temporal logic with bounded operators, in which the specification and analysis is based on the reachability graph constructed via TCPNs. The advantage of RGL over other temporal logics is the reduction of analysis complexity.