Title :
Problem decomposition and sub-model reconciliation of control systems in Event-B
Author :
Yeganefard, Sanaz ; Butler, Mairead
Author_Institution :
Electron. & Comput. Sci., Univ. of Southampton, Southampton, UK
Abstract :
To break the complexity of the formalisation process, we propose to model a functional requirement document of a control system as composeable monitored, controlled, mode and commanded sub-models. Influenced by the problem frame approach and the decomposition of the four-variable model, we suggest decomposing requirements of a control system into monitored, controlled, mode and commanded sub-problems. Each sub-problem can be formalised in a step-wise manner as a separate sub-model. To introduce the phenomena shared amongst the subproblems, the sub-models are reconciled. We propose a reconciliation process in the Event-B formal language based on the shared-variable and the shared-event styles which were originally developed for a model decomposition. The advantages and disadvantages of shared-variable and the shared-event reconciliation steps are also discussed. The requirements of an automotive cruise control system are decomposed and formalised as sub-models. These sub-models are also reconciled to introduce shared phenomena.
Keywords :
control engineering computing; formal languages; Event-B formal language; automotive cruise control system; control system submodel reconciliation; four-variable model decomposition; functional requirement document; problem decomposition; problem frame approach; shared-event reconciliation step; shared-variable reconciliation step; submodel reconciliation; Abstracts; Complexity theory; Control systems; Mathematical model; Monitoring; Software; Vehicles;
Conference_Titel :
Information Reuse and Integration (IRI), 2013 IEEE 14th International Conference on
Conference_Location :
San Francisco, CA
DOI :
10.1109/IRI.2013.6642515