Specification and Verification of Invariant Properties of Transition Systems

被引：8
|
作者：
Gaina, Daniel [1 ,2 ]
Tutu, Ionut [3 ,4 ]
Riesco, Adrian [5 ]
机构：
[1] Kyushu Univ, Fukuoka, Fukuoka, Japan
[2] La Trobe Univ, Melbourne, Vic, Australia
[3] Romanian Acad, Simion Stoilow Inst Math, Bucharest, Romania
[4] Royal Holloway Univ London, Egham, Surrey, England
[5] Univ Complutense Madrid, Madrid, Spain
来源：
2018 25TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2018) | 2018年
关键词：
algebraic specification; theorem proving; term rewriting; transition systems;
D O I：
10.1109/APSEC.2018.00024
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.
引用
收藏
页码：99 / 108
页数：10
相关论文
共 50 条
  • [1] SPECIFICATION AND VERIFICATION OF TIMING PROPERTIES IN INTEROPERABLE MEDICAL SYSTEMS
    Zarneshan, Mahsa
    Ghassemi, Fatemeh
    Khamespanah, Ehsan
    Sirjani, Marjan
    Hatcliff, John
    LOGICAL METHODS IN COMPUTER SCIENCE, 2022, 18 (02) : 1 - 13
  • [2] Quantitative Properties of Software Systems: Specification, Verification, and Synthesis
    Krstic, Srdan
    36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE COMPANION 2014), 2014, : 674 - 677
  • [3] Invariant-preserving transformations for the verification of place/transition systems
    Cheung, TY
    Zeng, W
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 1998, 28 (01): : 114 - 121
  • [4] On Verification of Interoperability of CAD Systems with a Focus on Invariant Properties
    Sap, Duygu
    Shapiro, Vadim
    COMPUTER-AIDED DESIGN, 2019, 115 : 256 - 266
  • [5] Specification and formal verification of temporal properties of production automation systems
    Flake, Stephan
    Müller, Wolfgang
    Pape, Ulrich
    Ruf, Jürgen
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, 3147 : 206 - 226
  • [6] Specification and formal verification of temporal properties of production automation systems
    Flake, S
    Müller, W
    Pape, U
    Ruf, J
    INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 206 - 226
  • [7] Specification and Verification of Spatio-Temporal Properties of Mobile Systems
    Schaefer, Andreas
    IT-INFORMATION TECHNOLOGY, 2008, 50 (05): : 324 - 326
  • [8] SPECIFICATION AND VERIFICATION OF VLSI SYSTEMS
    WILK, A
    PNUELI, A
    1989 IEEE INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN: DIGEST OF TECHNICAL PAPERS, 1989, : 460 - 463
  • [9] Properties as processes: Their specification and verification
    Kelso, J
    Milne, G
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 503 - 517
  • [10] AUTOMATIC VERIFICATION OF PROPERTIES IN TRANSITION-SYSTEMS
    ARNOLD, A
    BRLEK, S
    SOFTWARE-PRACTICE & EXPERIENCE, 1995, 25 (06): : 579 - 596
12345