Wyniki wyszukiwania - BazTech

1

Modeling Group Scheduling Problems in Space and Time by Timed Petri Nets

Graff D., Richling J., Werner M.

Fundamenta Informaticae

|

2013

|

Vol. 122, nr 4

297--313

EN

Dealing with cyber-physical systems (CPS) puts a strong emphasis on the interaction between computing and non-computing elements. Since the physical world is characterized by being strongly distributed and concurrent, this is also reflected in the computational world making the design of such systems a challenging task. If a number of tasks shall be executed on a CPS which are bound to time and space, may have dependencies to other tasks and requires a specific amount of computing devices, a solution requires a four-dimensional space-time schedule which includes positioning of the devices resulting in an NP-hard problem. In this paper, we address the problem of spatial-temporal group scheduling using Timed Petri nets. We use Timed Petri nets in order to model the spatial, temporal, ordered and concurrent character of our mobile, distributed system. Our model is based on a discrete topology in which devices can change their location by moving from cell to cell. Using the time property of Petri nets, we model movement in a heterogeneous terrain as well as task execution or access to other resources of the devices. Given the modeling, we show how to find an optimal schedule by translating the problem into a shortest path problem, which is solvable with the known method of dynamic programming.

2

A Method to Prove Non-Reachability in Priority Duration Petri Nets

Werner M., Popova-Zeugmann L., Richling J.

Fundamenta Informaticae

|

2004

|

Vol. 61, nr 3,4

351--368

EN

Times and priorities are important concepts that are frequently used to model real-world systems. Thus, there exist extensions for Petri nets which allow to model times and priorities. In contrast, many proof techniques are based on classical (time-less and priority-less) Petri nets. However, this approach fails frequently for timed and prioritized Petri nets. In this paper, we present an approach to prove non-reachability in a Priority Duration Petri net. We use for this proving technique a state equation as well as conditions for firing that include a priority rule and a maximal step rule. Our approach leads to a system of equations and inequalities, which provide us with a sufficient condition of non-reachability. We demonstrate the application of our approach with an example

3

Using State Equation to Prove Non-Reachability in Timed Petrinets

Popova-Zeugmann L., Werner M., Richling J.

Fundamenta Informaticae

|

2003

|

Vol. 55, nr 2

187-202

EN

Non-reachability proofs in Timed Petrinets were usually done by proving the non-reachability within the underlying timeless net. However, in many cases this approach fails. In this paper, we present an approach to prove non-reachability within the actual Timed Petrinet. For this purpose, we introduce a state equation for Timed Petrinets in analogy to timeless nets. Using this state equation, we can express reachability as a system of equations and inequations, which is solvable in polynomial time.

4

Verification of Non-functional Properties of a Composable Architecture with Petrinets

Richling J., Popova-Zeugmann L., Werner M.

Fundamenta Informaticae

|

2002

|

Vol. 51, nr 1,2

185-200

EN

In this paper, we introduce our concept of composability and present the MSS architecture as an example for a composable architecture. MSS claims to be composable with respect to timing properties. We discuss, how to model and prove properties in such an architecture with time-extended Petrinets. As a result, the first step of a proof of composability is presented as well as a new kind of Petrinet, which is more suitable for modeling architectures like MSS.