摘要: This paper presents a formal approach to the specification, construction and automated verification of large software systems. We describe design methodology, theory correctness, proof strategy for resulting obligations, experiences from case studies carried out using Karlsruhe Interactive Verifier (KIV). The methodology supports top-down development structured algebraic first-order specifications stepwise implementation its parts by program modules. correctness modular systems is proved be compositional. For single modules we give characterization in terms Dynamic Logic. provides general solution problem implementations full specifications.
springer.com
sci-hub.st 参考文章(22)
M. AdelsonVelskii, AN ALGORITHM FOR THE ORGANIZATION OF INFORMATION ,(1963)
Hartmut Ehrig, Bernd Mahr, Fundamentals of Algebraic Specification 1: Equations and Initial Semantics ,(1985)
David Harel, First-Order Dynamic Logic ,(1979)
N. Eisinger, H. J. Ohlbach, The Markgraf Karl Refutation Procedure (MKRP) conference on automated deduction. pp. 681- 682 ,(1986) , 10.1007/3-540-16780-3_135
S. Biundo, B. Hummel, D. Hutter, C. Walther, The Karlsruhe Induction Theorem Proving System conference on automated deduction. pp. 672- 674 ,(1986) , 10.1007/3-540-16780-3_132
G. Antoniou, V. Sperschneider, On the Verification of Modules computer science logic. pp. 16- 35 ,(1989) , 10.1007/3-540-52753-2_30
Bill Pase, Sentot Kromodimoeljo, m-NEVER System Summary conference on automated deduction. pp. 738- 739 ,(1988) , 10.1007/BFB0012874
J. Goguen, J. Meseguer, Universal Realization, Persistent Interconnection and Implementation of Abstract Modules international colloquium on automata, languages and programming. pp. 265- 281 ,(1982) , 10.1007/BFB0012775
V. Giarratana, F. Gimona, U. Montanari, Observability concepts in abstract data type specification mathematical foundations of computer science. pp. 576- 587 ,(1976) , 10.1007/3-540-07854-1_231
Hartmut Ehrig, Bernd Mahr, Fundamentals of Algebraic Specification 2: Module Specifications and Constraints ,(2011)