Automatic Integration of Safety Invariants into Z Specifications
R. Heckel, M. Conrad, G. Egger, J. Hiemer, in: Proceedings of the Workshop on Tools for System Development and Verifcation, Shaker Verlag, Bremen, Germany, 1996, pp. 70–83.
Download
No fulltext has been uploaded.
Conference Paper
| English
Author
Heckel, Reiko;
Conrad, Mirko;
Egger, Gottfried;
Hiemer, Jörg
Department
Abstract
This extended abstract describes a mechanism to automatically incorporate safety requirements into operational specifications written in Z. For every individual operation the global (i.e. operation independent) safety invariants are transformed into a predicate which is used to extend the original precondiction of the operation. The operation constructed this way shows the same beavior as the original one whenever its post state satisfies the invariant. Otherwise it refuses to do anything. The construction of the precondition can be carried out automatically and a corresponding tool development is in progress.
Publishing Year
Proceedings Title
Proceedings of the Workshop on Tools for System Development and Verifcation
Volume
1
Page
70-83
LibreCat-ID
Cite this
Heckel R, Conrad M, Egger G, Hiemer J. Automatic Integration of Safety Invariants into Z Specifications. In: Proceedings of the Workshop on Tools for System Development and Verifcation. Vol 1. Bremen, Germany: Shaker Verlag; 1996:70-83.
Heckel, R., Conrad, M., Egger, G., & Hiemer, J. (1996). Automatic Integration of Safety Invariants into Z Specifications. In Proceedings of the Workshop on Tools for System Development and Verifcation (Vol. 1, pp. 70–83). Bremen, Germany: Shaker Verlag.
@inproceedings{Heckel_Conrad_Egger_Hiemer_1996, place={Bremen, Germany}, title={Automatic Integration of Safety Invariants into Z Specifications}, volume={1}, booktitle={Proceedings of the Workshop on Tools for System Development and Verifcation}, publisher={Shaker Verlag}, author={Heckel, Reiko and Conrad, Mirko and Egger, Gottfried and Hiemer, Jörg}, year={1996}, pages={70–83} }
Heckel, Reiko, Mirko Conrad, Gottfried Egger, and Jörg Hiemer. “Automatic Integration of Safety Invariants into Z Specifications.” In Proceedings of the Workshop on Tools for System Development and Verifcation, 1:70–83. Bremen, Germany: Shaker Verlag, 1996.
R. Heckel, M. Conrad, G. Egger, and J. Hiemer, “Automatic Integration of Safety Invariants into Z Specifications,” in Proceedings of the Workshop on Tools for System Development and Verifcation, 1996, vol. 1, pp. 70–83.
Heckel, Reiko, et al. “Automatic Integration of Safety Invariants into Z Specifications.” Proceedings of the Workshop on Tools for System Development and Verifcation, vol. 1, Shaker Verlag, 1996, pp. 70–83.
Google Scholar