The paper discusses a constructive approach to the temporal logic specification and analysis of dependability requirements of automation systems. The work is based on TRIO formal method, which supports a declarative temporal logic language with a linear notion of time, and makes use of UML class diagrams to describe the automation system. The {\em general} concepts presented for the automation system {\em domain} are here {\em instantiated} on a case study {\em application} taken from the energy distribution field.