Abstract
This paper puts forward a new approach for the specification and verification of finite state systems. The design of a system is first specified in UML statechart diagrams, then formalized in the 𝜋-calculus and finally verified automatically by NuSMV. We demonstrate an application of the proposed approach using the SET/A protocol as an example.