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
来源：
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS | 2008年 / 5140卷
关键词：
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 条
  • [41] Towards a Broader Acceptance of Formal Verification Tools The Role of Education
    Khazeev, Mansur
    Mazzara, Manuel
    Aslam, Hamna
    de Carvalho, Daniel
    IMPACT OF THE 4TH INDUSTRIAL REVOLUTION ON ENGINEERING EDUCATION, ICL2019, VOL 2, 2020, 1135 : 188 - 200
  • [42] Compositional verification using SVL scripts
    Lang, F
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 465 - 469
  • [43] Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler
    Lawall, Julia
    Nishimura, Keisuke
    Lozi, Jean-Pierre
    STATIC ANALYSIS, SAS 2024, 2025, 14995 : 194 - 215
  • [44] Towards the Formal Verification of a Java']Java Processor in Event-B
    Evans, Neil
    Grant, Neil
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 201 : 45 - 67
  • [45] Towards Formal Verification of Reset Sequence in Fully Asynchronous Digital Circuits
    Melnychenko, Oleksandr
    Kreuter, Hans-Peter
    2014 10TH CONFERENCE ON PH.D. RESEARCH IN MICROELECTRONICS AND ELECTRONICS (PRIME 2014), 2014,
  • [46] A first step towards formal verification of security policy properties for RBAC
    Drouineaud, M
    Bortin, M
    Torrini, P
    Sohr, K
    QSIC 2004: PROCEEDINGS OF THE FOURTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2004, : 60 - 67
  • [47] Formal Verification
    Meenakshi, B.
    RESONANCE-JOURNAL OF SCIENCE EDUCATION, 2005, 10 (05): : 26 - 38
  • [48] Towards establishing formal verification and inductive code synthesis in the PLC domain
    Weiss, Matthias
    Marks, Philipp
    Maschler, Benjamin
    White, Dustin
    Kesseli, Pascal
    Weyrich, Michael
    2021 IEEE 19TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2021,
  • [49] Towards the Formal Verification of a Java']Java Processor in Event-B
    Grant, Neil
    Evans, Neil
    WOTUG-30: COMMUNICATING PROCESS ARCHITECTURES 2007, 2007, 65 : 425 - 442
  • [50] Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification
    Matichuk, Daniel
    Murray, Toby
    Andronick, June
    Jeffery, Ross
    Klein, Gerwin
    Staples, Mark
    2015 IEEE/ACM 37TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, VOL 1, 2015, : 722 - 732
12345