Séminaires
Séminaire du 21 Mars 2008
Lieu
CNAM: comment y aller
Programme
14h00-15h00: Hanifa Boucheneb - Ecole Polytechnique de Montréal (invitée au Cnam), "Model checking timed linear properties of time Petri nets using the state class method" (abstract ci-joint)
Abstract: we consider time Petri nets (TPN) and show how to efficiently model check timed linear properties, using the TPN state class graph method (SCG) and a time extension of Büchi automata (BA). We first establish a relation of bisimulation over the SCG which induces more compact graph (CSCG) preserving linear properties of the model. Afterwards, we propose an extension to Büchi automata, called Interval Timed Büchi Automata (ITBA), which is more appropriate than timed Büchi automata (TBA). Indeed, in the TBA, time requirements are expressed by means of clocks whereas they are expressed using delays in the CSCG. In addition, in the CSCG, exact firing delays are abstracted and only distances between delays are kept.
An ITBA is a BA extended with a set of real-valued delays, a set of intervals associated with delays, guards and actions associated with edges. Guards of edges specify the position of their firing time relatively to intervals associated with delays (before, in, before exit, after). Actions may deactivate or (re)activate delays. The intuition is that these delays act as timers used to constraint the validity duration of properties, expressed in terms of intervals.
15h00-15h30 : Awatef HICHEUR (Cedric-CNAM): "Timed Recursive ECATNets : Application to analysis of timed-constrained reconfigurable workflow processes"
Abstract: Nowadays, to stay competitive, companies are more and more adopting the workflow management systems (WfMSs for short) technology, for automating, monitoring and improving their critical business processes. Among the limitations of current workflow products and languages, one can note that only few of the WfMSs provide efficient ways of managing flexible workflows, which require dynamic reconfiguration of their structure at the occurrence of exceptional situations. Particularly, the current trend of business globalisation (where multiple parties belonging to different companies collaborate in a business process) brings new challenges regarding the flexibility of workflow processes. If we want to describe, in a faithful manner, flexible and collaborative workflow processes, we need modeling formalisms that offer mechanisms allowing us to manage dynamic structural changes and to describe both the dependencies between the process tasks and the distributed execution of the process over collaborative partners. Moreover, temporal feature is an important attribute of workflow specifications e.g. activity durations or deadlines. It is also crucial to be able to detect the violation of these time constraints during workflow execution or to calculate the overall process duration. In order to tackle this question, we introduce a new model, namely, Timed Recursive ECATNets (T-RECATNets). T-RECATNets are an extension of the ordinary Recursive ECATNets with time intervals associated to elementary transitions describing the minimum and the maximum duration of the firing action of these transitions. In this talk, we present first the semantics of T-RECATNets in terms of rewriting logic by means of real time rewrite theories. Consequently, using the Real Time Maude tool (a rewriting logic language implementation supporting the specification of real time systems), it is possible to create rapid prototypes of the developed T-RECATNet specifications on which various simulation and formal analysis techniques can be applied. Finally, we show the interest of our model in modelling timed–constrained reconfigurable workflow processes which operate on distributed execution environments.