Deductive Model Refinement

被引:0
|
作者
Smith, Douglas R. [1 ]
Nedunuri, Srinivas [2 ]
机构
[1] Kestrel Inst, Palo Alto, CA 94304 USA
[2] Sandia Natl Labs, Livermore, CA 94550 USA
来源
NASA FORMAL METHODS, NFM 2024 | 2024年 / 14627卷
关键词
Refinement; model-based design; formal specification; reactive synthesis; function synthesis; program synthesis;
D O I
10.1007/978-3-031-60698-4_9
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Deductive model refinement (hereafter simply "model refinement") is a uniform approach to generating correct-by-construction designs for algorithms and systems from formal specifications. Given an overapproximating model M of system dynamics and a set phi of required properties, model refinement is an iterative process that eliminates behaviors of M that do not satisfy the required properties. The result of model refinement is a refined model M' that satisfies by construction the required properties F. The calculations needed to generate refinements of M typically involve quantifier elimination and extensive formula/term simplification modulo the underlying domain theories. This paper focuses on the enforcement of basic safety properties in the form of state, action, and path invariants. We have run a prototype implementation of model refinement based on the Z3 SMT solver over a variety of system and algorithm design problems.
引用
收藏
页码:147 / 165
页数:19
相关论文
共 50 条
  • [1] DEDUCTIVE REFINEMENT OF SPECIES LABELLING IN WEAKLY LABELLED BIRDSONG RECORDINGS
    Morfi, Veronica
    Stowell, Dan
    2017 IEEE INTERNATIONAL CONFERENCE ON ACOUSTICS, SPEECH AND SIGNAL PROCESSING (ICASSP), 2017, : 656 - 660
  • [2] Deductive Model Checking
    Henny B. Sipma
    Tomás E. Uribe
    Zohar Manna
    Formal Methods in System Design, 1999, 15 : 49 - 74
  • [3] Deductive model checking
    Sipma, HB
    Uribe, TE
    Manna, Z
    FORMAL METHODS IN SYSTEM DESIGN, 1999, 15 (01) : 49 - 74
  • [4] THE PARTITION MODEL - A DEDUCTIVE DATABASE MODEL
    SPYRATOS, N
    ACM TRANSACTIONS ON DATABASE SYSTEMS, 1987, 12 (01): : 1 - 37
  • [5] A MODEL FOR MANIPULATION OF DEDUCTIVE DATABASES
    CAO, H
    BELL, DA
    HULL, MEC
    IRISH JOURNAL OF PSYCHOLOGY, 1993, 14 (03): : 505 - 507
  • [6] ANOTHER DEFENSE OF DEDUCTIVE MODEL
    HAUSMAN, DB
    SOUTHWESTERN JOURNAL OF PHILOSOPHY, 1976, 7 (01): : 111 - 117
  • [7] A KNOWLEDGE MODEL FOR UNIFYING DEDUCTIVE AND NON-DEDUCTIVE HETEROGENEOUS DATABASES
    SIROUNIAN, L
    GROSKY, WI
    IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 1995, 7 (01) : 82 - 105
  • [8] THE DEDUCTIVE MODEL - DOES IT HAVE INSTANCES
    KYBURG, H
    MINNESOTA STUDIES IN THE PHILOSOPHY OF SCIENCE, 1983, 10 : 299 - 312
  • [9] Verifying Invariants by Deductive Model Checking
    Bae, Kyungmin
    Escobar, Santiago
    Lopez-Rueda, Raul
    Meseguer, Jose
    Sapina, Julia
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2024, 2024, 14953 : 3 - 21
  • [10] Model refinement
    Sarah Seton-Rogers
    Nature Reviews Cancer, 2015, 15 (9) : 511 - 511