Verifying duration properties of timed transition systems

Zhiming Liu; Anders P. Ravn; Xiaoshan Li

Verifying duration properties of timed transition systems

Zhiming Liu, Anders P. Ravn, Xiaoshan Li

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

This paper proposes a method for formal real-time systems development:Requirements and high level design decisions are time interval properties and are therefore specified in the Duration Calculus (DC), while implementations are described bytimed transition systems (TTS). A link from implementation properties tothe requirement and design properties is given by interpreting a DC formula in a model of the executions of a TTS andthen providing rules for lifting properties proved by structuralinduction for a TTS to DC formulas. The method is illustrated by the Gas Burner case study.

Original language	English
Title of host publication	Proceedings of the IFIP Working Conference on Programming Concepts and Methods
Publisher	Chapman & Hall
Publication date	1998
Pages	327-345
Publication status	Published - 1998
Event	PROCOMET'98 - Duration: 1 Jan 1998 → …

Conference

Conference	PROCOMET'98
Period	01/01/1998 → …

OpenUrl availability

Full text

Cite this

@inproceedings{8548b17b7f12417db3e408b5ddacefaa,

title = "Verifying duration properties of timed transition systems",

abstract = "This paper proposes a method for formal real-time systems development:Requirements and high level design decisions are time interval properties and are therefore specified in the Duration Calculus (DC), while implementations are described bytimed transition systems (TTS). A link from implementation properties tothe requirement and design properties is given by interpreting a DC formula in a model of the executions of a TTS andthen providing rules for lifting properties proved by structuralinduction for a TTS to DC formulas. The method is illustrated by the Gas Burner case study.",

author = "Zhiming Liu and Ravn, \{Anders P.\} and Xiaoshan Li",

year = "1998",

language = "English",

pages = "327--345",

booktitle = "Proceedings of the IFIP Working Conference on Programming Concepts and Methods",

publisher = "Chapman \& Hall",

note = "PROCOMET'98 ; Conference date: 01-01-1998",

}

TY - GEN

T1 - Verifying duration properties of timed transition systems

AU - Liu, Zhiming

AU - Ravn, Anders P.

AU - Li, Xiaoshan

PY - 1998

Y1 - 1998

N2 - This paper proposes a method for formal real-time systems development:Requirements and high level design decisions are time interval properties and are therefore specified in the Duration Calculus (DC), while implementations are described bytimed transition systems (TTS). A link from implementation properties tothe requirement and design properties is given by interpreting a DC formula in a model of the executions of a TTS andthen providing rules for lifting properties proved by structuralinduction for a TTS to DC formulas. The method is illustrated by the Gas Burner case study.

AB - This paper proposes a method for formal real-time systems development:Requirements and high level design decisions are time interval properties and are therefore specified in the Duration Calculus (DC), while implementations are described bytimed transition systems (TTS). A link from implementation properties tothe requirement and design properties is given by interpreting a DC formula in a model of the executions of a TTS andthen providing rules for lifting properties proved by structuralinduction for a TTS to DC formulas. The method is illustrated by the Gas Burner case study.

M3 - Article in proceedings

SP - 327

EP - 345

BT - Proceedings of the IFIP Working Conference on Programming Concepts and Methods

PB - Chapman & Hall

T2 - PROCOMET'98

Y2 - 1 January 1998

ER -