In this paper, we consider subscript TCTL for Time Petri Nets (TPN-TCTL) for which temporal operators are extended with a time interval, specifying a time constraint on the firing sequences. We prove that the model-checking of a TPN-TCTL formula on a bounded TPN is decidable and is a PSPACE-complete problem. We propose a zone based state space abstraction that preserves marking reachability and traces of the TPN. As for Timed Automata (TA), the abstraction may use an over-approximation operator on zones to enforce the termination. A coarser (and efficient) abstraction is then provided and proved exact w.r.t. marking reachability and traces (LTL properties). Finally, we consider a subset of TPN-TCTL properties for which it is possible to propose efficient on-the-fly model-checking algorithms. Our approach consists in computing and exploring the zone based state space abstraction.

At the border between control and verification, parametric verification can be used to synthesize constraints on the parameters to ensure that a system verifies given specifications. In this paper we propose a new framework for the parametric verification of time Petri nets with stopwatches. We first introduce a parametric extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters and we define a symbolic representation of the parametric state-space based on the classical state-class graph method. Then, we propose semi-algorithms for the parametric modelchecking of a subset of parametric TCTL formulae on ITPNs. These results have been implemented in the tool Romeo and we illustrate them in a case-study based on a scheduling problem.

In this paper, we propose a method for the verification of timed properties for real-time systems featuring a preemptive scheduling policy: the system, modeled as a scheduling time Petri net, is first translated into a linear hybrid automaton to which it is time-bisimilar. Timed properties can then be verified using . The efficiency of this approach leans on two major points: first, the translation features a minimization of the number of variables (clocks) of the resulting automaton, which is a critical parameter for the efficiency of the ensuing verification. Second, the translation is performed by an over-approximating algorithm, which is based on Difference Bound Matrix and therefore efficient, that nonetheless produces a time-bisimilar automaton despite the over-approximation. The proposed modeling and verification method are generic enough to account for many scheduling policies. In this paper, we specifically show how to deal with Fixed Priority and Earliest Deadline First policies, with the possibility of using Round-Robin for tasks with the same priority. We have implemented the method and give some experimental results illustrating its efficiency.

Safety analysis in Systems Engineering (SE) processes, as usually implemented, rarely relies on formal methods such as model checking since such techniques, however powerful and mature, are deemed too complex for efficient use. This paper thus aims at improving the verification practice in SE design: considering the widely-used model of EFFBDs (Enhanced Function Flow Block Diagrams), it formally establishes its syntax and behavioral semantics. It also proposes a structural translation of EFFBDs to transition time Petri nets (TPNs); this translation is then proved to preserve the behavioral semantics (i.e. timed bisimilarity). After proving results on the boundedness of the resulting TPNs, it was possible to extend a number of fundamental properties (such as the decidability of liveness, state-access, etc.) from bounded TPNs to so-called bounded EFFBDs. Finally, these results led to implement and integrate an operational formal verification tool within a development platform, used in systems design for defense applications, where the underlying complexity is totally concealed from the end-user.

In this paper, we consider safe Time Petri Nets where time intervals (strict and large) are associated with places (TPPN), arcs (TAPN) or transitions (TTPN). We give the formal strong and weak semantics of these models in terms of Timed Transition Systems. We compare the expressiveness of the six models w.r.t. (weak) timed bisimilarity (behavioral semantics). The main results of the paper are : (i) with strong semantics, TAPN is strictly more expressive than TPPN and TTPN ; (ii) with strong semantics TPPN and TTPN are incomparable ; (iii) TTPN with strong semantics and TTPN with weak semantics are incomparable. Moreover, we give a complete classification by a set of 9 relations explained in a figure.

Several extensions of Time Petri nets (TPNs) have been proposed for modeling suspension and resumption of actions in timed systems. We first introduce a simple class of TPNs extended with stopwatches (SwTPNs), and present a semi-algorithm for building exact representations of the behavior of SwTPNs. Then, we prove that state reachability in SwTPNs and all similar models is undecidable, even when bounded, which solves an open problem. Finally, we discuss overapproximation methods yielding finite abstractions of their behavior for a subclass of bounded SwTPNs, and propose a new one based on a quantization of the polyhedra representing temporal information. By, adjusting a parameter, the exact behavior can be approximated as closely as desired.

We present in this paper a forward zone-based algorithm to compute the state space of a bounded Time Petri Net: the method is different and more efficient than the classical State Class Graph. We prove the algorithm to be exact with respect to the reachability problem. Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved to be timed bisimilar to the original Time Petri Net.

In order to analyze whether timing requirements of a real-time application are met, we propose an extension of the T-time Petri net model which takes into account the scheduling of the software tasks distributed over a multi-processor hardware architecture. The paper is concerned with static priority pre-emptive based scheduling. This extension consists in mapping into the Petri net model the way the different schedulers of the system activate or suspend the tasks. This relies on the introduction of two new attributes for the places (allocation and priority). First we give the formal semantics of this extended model as a timed transition system (TTS). Then we propose a method for its analysis consisting in the computation of the state class graph. Thus the verification of timing properties can be conducted (possibly together with an observator) and comes to analyze the such obtained state class graph.