Encoding a process algebra using the Event B method
| 详细信息 | 推荐本文 | |
- 作者：Yamine Ait-Ameur ; Mickael Baron ; Nadjet Kamel and Jean-Marc Mota
- 关键词：Event B method ; Refinements ; Process algebra ; Human– ; computer interaction ; User tasks validation
- 刊名：International Journal on Software Tools for Technology Transfer (STTT)
- 出版时间：July, 2009
- 出版年：2009
- 期刊代码：74_1433-2779
- 类别：cp
- 卷：11
- 期：3
- 页码：239-253
- 数据来源：sp
摘要
This paper presents the use of the B technique in its event based definition. We show that it is possible to encode, using Event B, the models (i.e., transition systems) associated to a process algebra with asynchronous semantics. The obtained Event B models consider that the Event B model associated to the left hand side of a BNF rule defining the algebra expressions is refined by a model corresponding to the right hand side of the same rule. The translation rules of each operator of a basic process algebra are given. Then, an example illustrating each translation rule is given. This approach is based on a proof technique and therefore it does not suffer from the state number explosion problem occurring in classical model checking. The interest of this work is the capability to validate user tasks or scenarios when using a given system and particularly a critical system. Finally, we discuss the application of this approach for validating user interfaces tasks in the human–computer interaction area.