A MODEL PARAMETRIC REAL-TIME LOGIC

被引：27

作者：

MORZENTI, A

MANDRIOLI, D

GHEZZI, C

机构：

[1] Politecnico di Milano, Milan

[2] Politecnico di Milano, Milan

[3] Politecnico di Milano, Milan

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 1992年 / 14卷 / 04期

关键词：

1ST-ORDER LOGIC; FORMAL SPECIFICATIONS; MODEL-THEORETIC SEMANTICS; REAL-TIME SYSTEMS; REQUIREMENTS VALIDATION; TEMPORAL LOGIC;

D O I：

10.1145/133233.129397

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

TRIO is a formal notation for the logic-based specification of real-time systems. In this paper the language and its straightforward model-theoretic semantics are briefly summarized. Then the need for assigning a consistent meaning to TRIO specifications is discussed, with reference to a variety of underlying time structures such as infinite-time structures (both dense and discrete) and finite-time structures. The main motivation is the ability to validate formal specifications. A solution to this problem is presented, which gives a new, model-parametric semantics to the language. An algorithm for constructively verifying the satisfiability of formulas in the decidable cases is defined, and several important temporal properties of specifications are characterized.

引用

页码：521 / 573

页数：53

共 34 条

[21]

Morzenti A., 1989, Proceedings Euromicro Workshop on Real Time (Cat. No.89TH0256-8), P26, DOI 10.1109/EMWRT.1989.43437

[22]

MORZENTI A, 1990, TRIO SPECIFICATION M

[23]

MORZENTI A, 1989, THESIS POLITECNICO M

[24]

MOSZKOWSKI B, 1985, COMPUTER, V18, P10, DOI 10.1109/MC.1985.1662795

[25]

Narayana K. T., 1988, Proceedings. Real-Time Systems Symposium (IEEE Cat. No.88CH2618-7), P86, DOI 10.1109/REAL.1988.51104

[26]

Ostroff J. S., 1987, Proceedings of the Real-Time Systems Symposium (Cat. No.87CH2475-2), P124

[27]

Ostroff J. S., 1989, ADV SOFTWARE DEV SER

[28] PROVING LIVENESS PROPERTIES OF CONCURRENT PROGRAMS [J].

OWICKI, S ;

LAMPORT, L .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1982, 4 (03) :455-495

[29] THE TEMPORAL SEMANTICS OF CONCURRENT PROGRAMS [J].

PNUELI, A .

THEORETICAL COMPUTER SCIENCE, 1981, 13 (01) :45-60

[30]

Rescher N., 1971, TEMPORAL LOGIC

← 1 2 3 4 →