  A model of an information system describes its processes and how resources
are involved in these processes to manipulate data objects. This paper presents
an extension to the Petri nets formalism suitable for describing information
systems in which states refer to object instances of predefined types and
resources are identified as instances of special object types. Several
correctness criteria for resource- and object-aware information systems models
are proposed, supplemented with discussions on their decidability for
interesting classes of systems. These new correctness criteria can be seen as
generalizations of the classical soundness property of workflow models
concerned with process control flow correctness.
