Petri nets and Activity Diagrams in logic controller specification - transformation and verification

The paper presents formal verification method of logic controller specification taking into account user-specified properties. Logic controller specification may be expressed as Petri net or UML 2.0 Activity Diagram. Activity Diagrams seem to be more user-friendly and easy-understanding that Petri nets. Specification in form of activity diagram may afterwards be transformed into Petri net, which may then be formally verified and used to automatically generate implementation (code). Verification process is executed automatically by model checker tools. Model description based on specification and properties list is being built. Properties are defined using temporal logic. In model checking process, verification tool NuSMV checks whether requirements are satisfied in attached system model. If this is not the case, appropriate counterexamples are generated.