|
|
|
篇目详细内容 |
|
【篇名】 |
Property transformation under specification change |
|
【刊名】 |
Frontiers of Computer Science in China |
|
【刊名缩写】 |
Front. Comput. Sci. China |
|
【ISSN】 |
1673-7350 |
|
【EISSN】 |
1673-7466 |
|
【DOI】 |
10.1007/s11704-010-0112-5 |
|
【出版社】 |
Higher Education Press and Springer-Verlag Berlin
Heidelberg |
|
【出版年】 |
2011 |
|
【卷期】 |
5
卷1期 |
|
【页码】 |
1-13
页,共
13
页 |
|
【作者】 |
Zheng FU;
Graeme SMITH;
|
|
【关键词】 |
formal methods; Z; refinement; temporal logic; system property |
【摘要】 |
|
Formal specifications of software systems need to evolve in many ways during system development. Not only are changes required to refine the specification toward an implementation, they are also required in response to changes in requirements, or to incorporate different aspects of the system, e.g., fault tolerance or timing, initially ignored in order to simplify reasoning. This paper presents an approach for evolving Z specifications by the step-wise application of a number of simple rules. These rules not only document the evolution of the specification, but also make precise how properties of the system evolve with the specification. Hence, reasoning about these properties performed on the original specification need not be repeated on the new specification. |
|
