A language for description and verification of mobile agent algorithms

Mobile agent technology has been widely adopted in network computing, whereas it remains a problem to design and verify the mobile agent algorithms in a platform independent way. In this paper, we propose a script language called SMAL to design the mobile agent algorithm. The semantics of SMAL is briefly introduced with its execution model. Furthermore, to verify the agent program in SMAL, a transformation function for converting SMAL program to Mobile UNITY specification is presented, which would facilitate making use of UNITY-logic to prove the correctness properties of the program.