Modeling logical and temporal conditions to formally validate factory automation web services
Corina Popescu, Jose Luis Martinez Lastra · 2007
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.