Modelling the Embedded Control System Using iUML-B Pattern State Machine

Developing the formal model based on the Event-B design pattern is an excellent method to improve the development efficiency of the embedded control system and improve the reusability of the formal model. However, the instantiation of the Event-B design pattern requires the manual writing of a large...

Full description

Saved in:
Bibliographic Details
Main Authors: Han Peng, Chenglie Du, Lei Rao, Zhouzhou Liu
Format: Article
Language:English
Published: Wiley 2018-01-01
Series:Journal of Control Science and Engineering
Online Access:http://dx.doi.org/10.1155/2018/1468172
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1832560923841134592
author Han Peng
Chenglie Du
Lei Rao
Zhouzhou Liu
author_facet Han Peng
Chenglie Du
Lei Rao
Zhouzhou Liu
author_sort Han Peng
collection DOAJ
description Developing the formal model based on the Event-B design pattern is an excellent method to improve the development efficiency of the embedded control system and improve the reusability of the formal model. However, the instantiation of the Event-B design pattern requires the manual writing of a large number of model codes, which brings a great deal of learning cost and coding burden to the engineering staff. In this paper, we propose a modelling approach for formal development of control systems based on the application of iUML-B state machine patterns to model the four synchronization patterns of the typical control system. Then, we use the instantiation of iUML-B pattern state machine to establish a typical multilevel control system's Event-B model. The simulation results show that the event trace of the model obtained using our method is the same as that of the corresponding model obtained using the traditional Event-B design pattern. Compared with the traditional Event-B design pattern method, our method can greatly reduce the manual coding burden in the modelling process. The system model expressed using the iUML-B pattern state machine can be easily mapped to the labelled transition system so as to verify the behavioural properties of the model.
format Article
id doaj-art-11a32e7acd1346b4b9de7fb3ecd16879
institution Kabale University
issn 1687-5249
1687-5257
language English
publishDate 2018-01-01
publisher Wiley
record_format Article
series Journal of Control Science and Engineering
spelling doaj-art-11a32e7acd1346b4b9de7fb3ecd168792025-02-03T01:26:16ZengWileyJournal of Control Science and Engineering1687-52491687-52572018-01-01201810.1155/2018/14681721468172Modelling the Embedded Control System Using iUML-B Pattern State MachineHan Peng0Chenglie Du1Lei Rao2Zhouzhou Liu3School of Computer Science, Northwestern Polytechnical University, Xi’an, ChinaSchool of Computer Science, Northwestern Polytechnical University, Xi’an, ChinaSchool of Software and Microelectronics, Northwestern Polytechnical University, Xi’an, ChinaSchool of Computer Science, Northwestern Polytechnical University, Xi’an, ChinaDeveloping the formal model based on the Event-B design pattern is an excellent method to improve the development efficiency of the embedded control system and improve the reusability of the formal model. However, the instantiation of the Event-B design pattern requires the manual writing of a large number of model codes, which brings a great deal of learning cost and coding burden to the engineering staff. In this paper, we propose a modelling approach for formal development of control systems based on the application of iUML-B state machine patterns to model the four synchronization patterns of the typical control system. Then, we use the instantiation of iUML-B pattern state machine to establish a typical multilevel control system's Event-B model. The simulation results show that the event trace of the model obtained using our method is the same as that of the corresponding model obtained using the traditional Event-B design pattern. Compared with the traditional Event-B design pattern method, our method can greatly reduce the manual coding burden in the modelling process. The system model expressed using the iUML-B pattern state machine can be easily mapped to the labelled transition system so as to verify the behavioural properties of the model.http://dx.doi.org/10.1155/2018/1468172
spellingShingle Han Peng
Chenglie Du
Lei Rao
Zhouzhou Liu
Modelling the Embedded Control System Using iUML-B Pattern State Machine
Journal of Control Science and Engineering
title Modelling the Embedded Control System Using iUML-B Pattern State Machine
title_full Modelling the Embedded Control System Using iUML-B Pattern State Machine
title_fullStr Modelling the Embedded Control System Using iUML-B Pattern State Machine
title_full_unstemmed Modelling the Embedded Control System Using iUML-B Pattern State Machine
title_short Modelling the Embedded Control System Using iUML-B Pattern State Machine
title_sort modelling the embedded control system using iuml b pattern state machine
url http://dx.doi.org/10.1155/2018/1468172
work_keys_str_mv AT hanpeng modellingtheembeddedcontrolsystemusingiumlbpatternstatemachine
AT chengliedu modellingtheembeddedcontrolsystemusingiumlbpatternstatemachine
AT leirao modellingtheembeddedcontrolsystemusingiumlbpatternstatemachine
AT zhouzhouliu modellingtheembeddedcontrolsystemusingiumlbpatternstatemachine