Issue title: Selected papers from the International Conference on Computer Science, Software Engineering, Information Technology, e-Business, and Applications, 2003
Affiliations: [a] Universidad Nacional de San Luis, Departamento de Informática, Ejército de los Andes 950, 5700 – San Luis, Argentina | [b] Department of Computer Science, Winona State University, Winona, MN 55987, USA
Abstract: PN (PN) are tools for the analysis and design of concurrent systems. There is a formal theory, which supports PN. An extension of PN is Petri Nets with Clocks (PNwC). PNwC are useful to model systems with temporal requirements via specification of clocks, using temporal invariants for the places and temporal conditions in the transitions. Using invariants in places allows the specifications of hard deadlines constrains (upper bound constrains): when a deadline is reached the progress of time is blocked by the invariant and the action becomes urgent. An algorithm for the analysis of a PNwC has been proposed in [1]. The algorithm is oriented to the verification and correction of errors in the modelling of the time variable. The algorithm generates information about temporal unreachable states and process deadlocks with temporal blocks. Also, it corrects places invariants and transitions conditions. We present here a formalism for PNwC based on Timed Graphs. The analysis algorithm is presented here using the formalism. We show here how Petri Net theory can be joined with Timed Graph theory to construct a formalism, which supports a tool for the analysis of models of concurrent process with real time specification.
Keywords: PN, timed graphs, timed PN, CASE tools, real time systems
