More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement
More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement
复制标题
更强大的 Z 数据细化：推动工业细化的最先进水平
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
J. Woodcock
中科院分区：
文献类型：
--
作者：
S. Stepney;David Cooper;J. Woodcock
我们最近完成了一个大型工业规模应用的规范和充分的细化证明。该应用程序对安全至关重要，进行建模和证明是为了增加客户的保证，即所实施的系统没有涉及安全问题的设计缺陷。在这里，我们描述的应用程序，然后讨论一个重要的教训，以了解有关大型证明合同：一个人必须建立一条道路之间的数学形式，一方面和实际实现的结果。我们提出了一些这样的决策点的例子，解释在每种情况下必须作出的考虑。
We have recently completed the specification and full refinement proof of a large, industrial scale application. The application was security critical, and the modelling and proof was done to increase the client’s assurance that the implemented system had no design flaws with security implications. Here we describe the application, and then discuss an essential lesson to learn concerning large proof contracts: that one must forge a path between mathematical formality on the one hand and practical achievement of results on the other. We present a number of examples of such decision points, explaining the considerations that must be made in each case.