{Specification, Execution and Verification of Interaction Protocols: an Approach based on Computational Logic}