The refinement of embedded software with the B-method
The refinement of embedded software with the B-method
复制标题
使用 B 方法细化嵌入式软件
DOI：
10.14236/ewic/fa1996.6
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
H. Treharne
中科院分区：
文献类型：
--
作者：
J. Draper;H. Treharne
本文介绍了在MIST项目中使用形式化精化。MIST（Measurable Improvement in Specification Techniques）是ESSI应用实验10228。这是一个为期18个月的项目，涉及三家公司：GEC-Marconi Avionics是主要用户; Praxis是主要分包商，担任独立评审员; B-Core（英国）提供所使用的工具和咨询。MIST的主要目的是开发实用程序，将形式化方法与安全关键航空电子软件开发的当前方法结合起来应用。
该论文描述了该项目开发的一种规范风格，该风格对系统上下文中的嵌入式软件进行建模。它还描述了一种细化风格，称为结构细化。本文说明了一个小的例子，并报告其应用程序的一个大的案例研究内的MIST项目。最初，在使用经过结构改进的企业工具包时遇到一些问题，但新的企业工具包克服了大多数问题。嵌入式规范风格工作得很好，允许嵌入式软件用抽象接口进行规范，用具体接口进行细化。结构上的改进使设计能够相当快地划分。总的来说，细化比预期的要容易，花了65天，而编写摘要规范需要48天。改进的证明是唯一实现的，因为设计已经被结构改进划分。
This paper describes the use of formal refinement within the MIST project. MIST (Measurable Improvement in Specification Techniques) is ESSI application experiment 10228. It is an 18 month project involving three companies: GEC-Marconi Avionics, who are the prime user; Praxis, who are the main subcontractor, acting as an independent reviewer; and B-Core (UK), who provide the tools used and consultancy. The main aim of MIST is to develop practical procedures for applying formal methods in conjunction with current methods for safety critical avionics software development.
The paper describes a specification style developed by the project that models embedded software within a systems context. It also describes a style of refinement, known as structural refinement. The paper illustrate both with a small example and also reports on their application to a large case study within the MIST project. Initially, there were some problems in using the B-Toolkit with structural refinement, but most of these were overcome by a new B-Toolkit. The embedded specification style worked well and allowed the embedded software to be specified with abstract interfaces and refined with concrete interfaces. The structural refinement allowed the design to be partitioned fairly quickly. Overall, refinement was easier than expected, taking 65 days compared to 48 days needed to write the abstract specification. The proof of the refinement was only achieved because the design had been partitioned by the structural refinement.