Interaksi mempelajari perilaku komponen di dalam sistem. Dalam sebuah sistem interaktif, karakteristik komponen mempengaruhi kinerja sistem. Dalam riset ini, metode untuk melakukan verifikasi interaksi dikenalkan menggunakan Coloured Petri Nets (CPN). Pertama, interaksi dimodelkan menggunakan diagram sekuen Unified Modeling Language (UML). Kemudian, diagram tersebut ditransformasikan menjadi model CPN. Untuk melakukannya, aturan transformasi dikenalkan. Interaksi di model CPN diverifikasi menggunakan teknik yang tersedia. Teknik tersebut antara lain: analisis state space , properti liveness, dan properti fairness. Selain itu, teknik dikenalkan untuk mengidentifikasi kesalahan dalam state space. Luaran dari riset ini adalah sebuah metode. Metode tersebut mempunyai tiga bagian penting. Bagian pertama adalah semantik formal dari diagram use case dan diagram sekuen. Semantik di definisikan dalam graf menggunakan gaya penulisan semantik denotasional. Bagian kedua adalah aturan transformasi yang mengubah diagram sekuen menjadi model CPN. Bagian ketiga adalah verifikasi model CPN. Verifikasi ini akan menunjukkan ada tidaknya kesalahan, yaitu kesalahan inisialisasi, kesalahan pascatugas, dan kesalahan urutan. Metode diterapkan pada studi kasus mesin penjaja coklat. Mesin ini merupakan contoh sistem interaktif yang kaya interaksi antara manusia dan mesin.