Abstract: RASA，an interactive protocol framework of MAS（Multi-agent System） put forward by Tim Miller in 2007，has been proved to better promote the interaction of MAS.However，this framework does not support the concurrency of MAS.Therefore，the thesis uses a conflict priority，that is，introducing an efficiency evaluation function to solve the problems which can not be determined in the state.Moreover，it expands the definition of RASA in order to support the concurrency.Then it adopts UPPAAL，an automatic verification tool based on time automation，and uses a very easy auction protocol to prove the feasibility of this approach.Finally，it describes a simple negotiation protocol and an auction protocol with RASA language to show the good characteristics of RASA protocol.

Key words: RASA, process algebra, constraint language, UPPAAL

摘要： RASA是2007年Tim Miller提出的一个MAS（Multi-agent System）交互协议框架，这个框架已被证明可以更好地促进MAS的交互，但此框架并不支持MAS的并发。利用了一种冲突优先方式，引入了效益评价函数来解决其状态无法确定的问题，并扩展了RASA的定义来支持其并发，随后采用了一种基于时间自动机的自动验证工具UPPAAL，利用一个简单的拍卖协议来验证这种方法的可行性。最后利用RASA语言描述了一个简单的协商协议和一个拍卖协议，以显示RASA协议的良好特性。

关键词: RASA, 进程代数, 约束语言, UPPAAL