Verification in factory and office automation

After considering the literature on verification in factory and office automation, the paper uses a timed Logic of Actions and Timestamp Petri Nets to specify processes. Proving techniques are introduced to verify a process realization against its specification. Afterwards, this approach to proving, which has been applied to technical problems in the past, is applied here to business processes. Finally, this transfer of results from factory to office automation is used to motivate further investigations in which results can be transferred between these research areas.