Encoding a process algebra using the Event B method: Application to the validation of human–computer interactions Export

@article{citeulike:4200095, abstract = {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.}, author = {Ait-Ameur, Yamine and Baron, Mickael and Kamel, Nadjet and Mota, Jean-Marc}, citeulike-article-id = {4200095}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/s10009-009-0109-2}, citeulike-linkout-1 = {http://www.springerlink.com/content/e678300406631434}, day = {18}, doi = {10.1007/s10009-009-0109-2}, issn = {1433-2787}, journal = {International Journal on Software Tools for Technology Transfer}, keywords = {2009, \_to\_appear, event-b, process\_algebra}, month = {March}, posted-at = {2009-03-21 02:10:27}, priority = {2}, title = {Encoding a process algebra using the Event B method: Application to the validation of human–computer interactions}, url = {http://dx.doi.org/10.1007/s10009-009-0109-2}, year = {2009} }

TY - JOUR ID - citeulike:4200095 L3 - citeulike-article-id:4200095 N2 - 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. JF - International Journal on Software Tools for Technology Transfer SN - 1433-2787 TI - Encoding a process algebra using the Event B method: Application to the validation of human–computer interactions KW - 2009 KW - _to_appear KW - event-b KW - process_algebra AU - Ait-Ameur, Yamine AU - Baron, Mickael AU - Kamel, Nadjet AU - Mota, Jean-Marc PY - 2009/03/18/ UR - http://dx.doi.org/10.1007/s10009-009-0109-2 ER -