THE EXISTENCE OF REFINEMENT MAPPINGS
THE EXISTENCE OF REFINEMENT MAPPINGS
复制标题
DOI：
10.1016/0304-3975(91)90224-p
复制
发表时间：
1991-05-31
影响因子：
1.1
通讯作者：
LAMPORT, L
中科院分区：
文献类型：
--
作者：
ABADI, M;LAMPORT, L
细化映射用于证明较低级别的规范正确实现了较高级别的规范。我们认为规范组成的状态机（这可能是无限状态），指定安全要求，和任意的补充属性，指定活性要求。从较低级别规范S1到较高级别规范S2的细化映射是从S1的状态空间到S2的状态空间的映射。它将S1状态机的步骤映射到S2状态机的步骤，并将S1允许的行为映射到S2允许的行为。我们表明，在合理的假设下的规格，如果S1实现S2，然后通过添加辅助变量到S1，我们可以保证存在一个细化映射。这提供了一个完整的结果，一个实用的，层次化的规范方法。
Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. We consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements, and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S1 to a higher-level one S2 is a mapping from S1's state space to S2's state space. It maps steps of S1's state machine to steps of S2's state machine and maps behaviors allowed by S1 to behaviors allowed by S2. We show that, under reasonable assumptions about the specifications, if S1 implements S2, then by adding auxiliary variables to S1 we can guarantee the existence of a refinement mapping. This provides a completeness result for a practical, hierarchical specification method.