Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B
Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B
复制标题
B 事件中巡航控制系统形式化建模指南的评估
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
K. Fode
中科院分区：
文献类型：
--
作者：
R. Rosenthal;K. Fode
最近，已经开发了一套指南或食谱，用于在事件-B中建模和完善控制问题。 Event-B形式方法用于通过定义对这些状态作用的系统和事件的状态来进行系统级建模。它还支持模型的改进。该食谱旨在通过区分环境，控制器和命令现象来系统化建模和完善控制问题系统的过程。本文中我们的主要目的是通过在汽车中发现的邮轮控制系统的正式建模中遵循该食谱，调查和评估该食谱的有用性和有效性。结果正在确定食谱的好处，并为其未来的用户提供指导。
Recently a set of guidelines, or cookbook, has been developed for modelling and refinement of control problems in Event-B. The Event-B formal method is used for system-level modelling by defining states of a system and events which act on these states. It also supports refinement of models. This cookbook is intended to systematise the process of modelling and refining a control problem system by distinguishing environment, controller and command phenomena. Our main objective in this paper is to investigate and evaluate the usefulness and effectiveness of this cookbook by following it throughout the formal modelling of cruise control system found in cars. The outcomes are identifying the benefits of the cookbook and also giving guidance to its future users.