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.
['Corina Popescu', 'Jose L. Martinez Lastra']
Modeling logical and temporal conditions to formally validate factory automation web services