Towards formal verification of TOOLBUS scripts

被引:0
|
作者
Fokkink, Wan [1 ]
Klint, Paul [1 ]
Lisser, Bert [1 ]
Usenko, Yaroslav S. [1 ]
机构
[1] Ctr Wiskunde & Informat, Amsterdam, Netherlands
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
TOOLBUS allows one to connect tools via a software bus. Programming is done using the scripting language TSCRIPT, which is based on the process algebra ACP. TSCRIPT was originally designed to enable formal verification, but this option has so far not been explored in any detail. We present a method for analyzing a TSCRIPT by translating it to the process algebraic language mCRL2, and then applying model checking to verify behavioral properties.
引用
下载
收藏
页码:160 / 166
页数:7
相关论文
共 50 条
  • [21] Formal Verification for Node-Based Visual Scripts Using Symbolic Model Checking
    Hasegawa, Isamu
    Yokogawa, Tomoyuki
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2022, E105D (01) : 78 - 91
  • [22] Towards Polynomial Formal Verification of Complex Arithmetic Circuits
    Drechsler, Rolf
    Mahzoon, Alireza
    Goli, Mehran
    2022 25TH INTERNATIONAL SYMPOSIUM ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS (DDECS), 2022, : 1 - 6
  • [23] Towards Formal Verification of Computations and Hypercomputations in Relativistic Physics
    Stannett, Mike
    MACHINES, COMPUTATIONS, AND UNIVERSALITY, MCU 2015, 2015, 9288 : 17 - 27
  • [24] Towards the Formal Verification of Cache Coherency at the Architectural Level
    Verbeek, Freek
    Schmaltz, Julien
    ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2012, 17 (03)
  • [25] Towards a Formal Verification Approach for Service Component Architecture
    Chargui, Wael
    Rouis, Taoufik Sakka
    Kmimech, Mourad
    Bhiri, Mohamed Tahar
    Sliman, Layth
    Raddaoui, Badran
    NEW TRENDS IN INTELLIGENT SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2017, 297 : 466 - 479
  • [26] Towards Formal Verification of a Commercial Wireless Router Firmware
    Lu, Zheng
    Steinmuller, Christopher
    Mukhopadhyay, Supratik
    2013 IEEE 37TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2013, : 639 - 647
  • [27] Towards a Formal Verification Approach for Cloud Software Architecture
    Ayach, Amal
    Sliman, Layth
    Kmimech, Mourad
    Bhiri, Mohamed Tahar
    Raddaoui, Badran
    NEW TRENDS IN INTELLIGENT SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2017, 297 : 490 - 502
  • [28] Towards Formal Verification of State Continuity for Enclave Programs
    Jangid, Mohit Kumar
    Chen, Guoxing
    Zhang, Yinqian
    Lin, Zhiqiang
    PROCEEDINGS OF THE 30TH USENIX SECURITY SYMPOSIUM, 2021, : 573 - 590
  • [29] Towards formal verification of cryptographic circuits: A functional approach
    Bitat, Abir
    Merniz, Salah
    2018 3RD INTERNATIONAL CONFERENCE ON PATTERN ANALYSIS AND INTELLIGENT SYSTEMS (PAIS), 2018, : 158 - 163
  • [30] Towards Formal Verification of Orchestration Computations Using the K Framework
    AlTurki, Musab A.
    Alzuhaibi, Omar
    FM 2015: FORMAL METHODS, 2015, 9109 : 40 - 56