Modeling logical and temporal conditions to formally validate factory automation web services

This paper is focused on presenting the means of modeling the conditions that are tested with either conditional or looping control constructs (repeat-while, repeat-until and if-then-else). The depicted ideas are part of a methodology developed to formally verify and validate the orchestration of factory automation web services. The formalism used to represent in a modular manner the sequencing of services is timed net condition/event systems (TNCES). The basic modules capable of modeling Boolean conditions are illustrated and initial ideas on how to represent timing conditions are sketched.