Finding inductive invariants is a key issue in many domains such as program verification, model based testing, etc. However, few approaches help the designer in the task of writing a correct and meaningful model, where correction is used for consistency of the formal specification w.r.t. its inner invariant properties. Meaningfulness is obtained by providing many explicit views of the model, like animation, counter-example extraction, and so on. We propose to ease the task of writing a correct and meaningful formal specification by combining a panel of provers, a set-theoretical constraint solver and some model-checkers. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Couchot, J. F., & Dadeau, F. (2007). Guiding the correction of parameterized specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4591 LNCS, pp. 176–194). Springer Verlag. https://doi.org/10.1007/978-3-540-73210-5_10
Mendeley helps you to discover research relevant for your work.