Development of adequate formalisms for verification of IEC 1499 distributed applications

Presents an attempt to bridge the gap between theoretical successes of formal methods and their actual application in engineering of industrial automation systems. It deals with modeling and verification of distributed control systems developed according to the being developed international standard IEC1499. A new modeling formalism of Signal/Net Systems (SNS) is suggested, which is a place/transition net with usual token-flow arcs from places to transitions and vice versa, as well as with event arcs from transitions to transitions, and condition arcs from places to transitions which correspondingly force or enable transitions without passing tokens. The distinct feature of the SNS is that complex models they can be easily composed in the modular way from the component modules. This formalism is developed with particular view on the modeling of closed-loop plant/controller systems. The controller is modeled in a full deterministic and synchronous way (all the transitions fire according to the earliest firing rule) as a non-timed place/transition net while the model of plant might have spontaneous transitions and discrete-timed arcs to model time consuming processes. Verification of the controller/plant closed-loop system includes investigation of reachability problems for standalone controller and object, as well as proving safety properties for the closed-loop system