文章基本信息

标题：Integration of B Activity into a Global Design Process of Critical Software
本地全文：下载
作者：Philippe Bon ; Philippe Bon ; Simon Collart-Dutilleul 等
期刊名称：Procedia - Social and Behavioral Sciences
印刷版ISSN：1877-0428
出版年度：2012
卷号：48
页码：2169-2178
DOI：10.1016/j.sbspro.2012.06.1190
语种：English
出版社：Elsevier
摘要：AbstractThe adequacy of the B method to produce a valid software implementation is well known, particularly in the guided transport domain. However, there is an important work to be performed using the informal specification before entering the B process. A lot of requirements are difficult to express and to assess using formal methods. The use of a human expertise cannot be avoided. The upstream requirements analysis may be assist with some graphical tool using UML notations. Nevertheless the main problem to be solved may be the choice of the adequate tool.Currently, there are several kinds of diagrams in the UML (Unified Meta Language) notation and they are partially redundant. Considering a more general point of view, an important human contribution is to choose the representation which is best adapted to the considered assessment problem. To give an example, before the implementation task, a global checking of the functional validity performed by an expert is relevant. In this case, a compact readable graphical model is useful. Furthermore, the dynamic aspects are better illustrated when this model can be simulated. High level Petri nets have both qualities of language power and formal modeling. Moreover, there are some dedicated simulation tools.The aim of this task is to provide a valid input into the B process. However, up to now, all requirements are not naturally integrated into the B process. Temporal requirements checking can be assisted using efficient tools.The assessment problem does not forbid using various complementary formalisms. The global approach consists in identifying which kind of services may be provided by a particular tool and to mix them with other ones in order to analyze a system. The model driven engineering (MDE) provides an interesting framework in order to transmit specifications and requirements from one representation to another.
关键词：Safe software design;transport systems;Model Driven Engineering;Formal methods