Induction in the Timed Interval Calculus

被引：1
|
作者：
Wabenhorst, A [1 ]
机构：
[1] Univ Queensland, Software Verificat Res Ctr, Brisbane, Qld 4072, Australia
来源：
THEORETICAL COMPUTER SCIENCE | 2003年 / 300卷 / 1-3期
关键词：
real-time specification and reasoning; interval logic; temporal logic; induction; timed traces;
D O I：
10.1016/S0304-3975(01)00378-4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The Timed Interval Calculus, a timed-trace formalism based on set theory, is introduced. It is extended with an induction law and a unit for concatenation, which facilitates the proof of properties over trace histories. The effectiveness of the extended Timed Interval Calculus is demonstrated via a benchmark case study, the mine pump. Specifically, a safety property relating to the operation of a mine shaft is proved, based on an implementation of the mine pump and assumptions about the environment of the mine. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：181 / 207
页数：27
相关论文
共 50 条
  • [1] A Verification System for Timed Interval Calculus
    Chen, Chunqing
    Dong, Jin Song
    Sun, Jun
    [J]. ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, 2008, : 271 - 280
  • [2] Machine-checking the Timed Interval Calculus
    Dawson, JE
    Goré, R
    [J]. AL 2002: ADVANCES IN ARTIFICIAL INTELLIGENCE, 2002, 2557 : 95 - 106
  • [3] Applying timed interval calculus to simulink diagrams
    School of Computing, National University of Singapore, Singapore
    [J]. Lect. Notes Comput. Sci, 2006, (74-93):
  • [4] Applying timed interval calculus to Simulink diagrams
    Chen, Chunqing
    Dong, Jin Song
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 74 - +
  • [5] Calculus for timed automata
    D'Argenio, P.R.
    Brinksma, E.
    [J]. 1996, (1135)
  • [6] A timed calculus for wireless systems
    Merro, Massimo
    Ballardin, Francesco
    Sibilio, Eleonora
    [J]. THEORETICAL COMPUTER SCIENCE, 2011, 412 (47) : 6585 - 6611
  • [7] Timed calculus of cryptographic communication
    Borgstoem, Johannes
    Grinchtein, Olga
    Kramer, Simon
    [J]. FORMAL ASPECTS IN SECURITY AND TRUST, 2007, 4691 : 16 - +
  • [8] A Logical Encoding of Timed π-Calculus
    Saeedloei, Neda
    [J]. LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2013, 2014, 8901 : 164 - 182
  • [9] A Timed Calculus for Wireless Systems
    Merro, Massimo
    Sibilio, Eleonora
    [J]. FUNDAMENTALS OF SOFTWARE ENGINEERING, 2010, 5961 : 228 - 243
  • [10] Themulus: A Timed Contract-calculus
    Garcia, Alberto Aranda
    Cambronero, Maria-Emilia
    Colombo, Christian
    Llana, Luis
    Pace, Gordon J.
    [J]. PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT (MODELSWARD), 2020, : 193 - 204
12345