Conference Proceeding
Details
Citation
Shankland C (1993) Automating (Specification = Implementation) using Equational Reasoning and LOTOS. In: Gaudel M & Jouannaud J (eds.) TAPSOFT'93: Theory and Practice of Software Development: 4th International Joint Conference CAAP/FASE Orsay, France, April 13–17, 1993 Proceedings. Lecture Notes in Computer Science, 668. TAPSOFT'93: 4th International Joint Conference CAAP/FASE, Orsay, France, 13.04.1993-17.04.1993. Berlin Heidelberg: Springer, pp. 544-558. http://link.springer.com/chapter/10.1007/3-540-56610-4_88; https://doi.org/10.1007/3-540-56610-4_88
Abstract
We explore some of the problems of verification by trying to prove that some sort of relationship holds between a given specification and implementation. We are particularly interested in the decisions taken in the process of establishing and formalising the verification requirements and of automating the proof. Despite the apparent simplicity of the original problem, the verification is non-trivial.
The example chosen is an abstraction of a real communications problem. We use the formal description technique LOTOS [8] for specification and implementation, and equational reasoning, automated by the RRL term rewriting system [9], for the proof.
Status | Published |
---|---|
Title of series | Lecture Notes in Computer Science |
Number in series | 668 |
Publication date | 31/12/1993 |
Publication date online | 30/04/1993 |
Publisher | Springer |
Publisher URL | http://link.springer.com/chapter/10.1007/3-540-56610-4_88 |
Place of publication | Berlin Heidelberg |
ISSN of series | 0302-9743 |
ISBN | 978-3-540-56610-6 |
Conference | TAPSOFT'93: 4th International Joint Conference CAAP/FASE |
Conference location | Orsay, France |
Dates | – |