Checking MSC specifications for timing inconsistency

被引：0

作者：

Li, XD ^{[1
]}

Tan, WK ^{[1
]}

Zheng, GL ^{[1
]}

机构：

[1] Nanjing Univ, Dept Comp Sci & Technol, State Key Lab Novel Software Technol, Nanjing 210093, Peoples R China

来源：

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY | 2002年 / 17卷 / 01期

关键词：

real-time system; message sequence chart; model checking; timing inconsistency;

D O I：

10.1007/BF02949824

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Message sequence chart (MSC) is a graphical and textual language for the description and specification of the interactions between system components. MSC specifications allow convenient expression of multiple scenarios, and offer an intuitive and visual way of describing design requirements. Like any other aspect of the specification and design process, MSCs are amenable to errors, and their analysis is important. In this paper, the verification problem of MSC specification for timing inconsistency is studied, which means that no execution scenario described by an MSC specification is timing consistent. An algorithm is developed to check MSC specifications for timing inconsistency.

引用

页码：47 / 55

页数：9

共 49 条

[41] Model checking time-dependent system specifications using Time Stream Petri Nets and UPPAAL [J].

Cicirelli, Franco ;

Furfaro, Angelo ;

Nigro, Libero .

APPLIED MATHEMATICS AND COMPUTATION, 2012, 218 (16) :8160-8186

[42] An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains [J].

Frenkel, Hadar ;

Grumberg, Orna ;

Sheinvald, Sarai .

JOURNAL OF AUTOMATED REASONING, 2019, 63 (04) :1077-1101

[43] An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains [J].

Hadar Frenkel ;

Orna Grumberg ;

Sarai Sheinvald .

Journal of Automated Reasoning, 2019, 63 :1077-1101

[44] Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more [J].

Plagge D. ;

Leuschel M. .

International Journal on Software Tools for Technology Transfer, 2010, 12 (1) :9-21

[45] The High Road to Formal Validation: Model Checking High-Level Versus Low-Level Specifications [J].

Leuschel, Michael .

ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, 2008, 5238 :4-23

[46] Improving timing analysis effectiveness for scenario-based specifications by combining SAT and LP techniques [J].

Lu, Longlong ;

Pan, Minxue ;

Zhang, Tian ;

Li, Xuandong .

SOFTWARE AND SYSTEMS MODELING, 2022, 21 (04) :1321-1338

[47] Improving timing analysis effectiveness for scenario-based specifications by combining SAT and LP techniques [J].

Longlong Lu ;

Minxue Pan ;

Tian Zhang ;

Xuandong Li .

Software and Systems Modeling, 2022, 21 :1321-1338

[48] Symbolic execution and timed automata model checking for timing analysis of Java']Java real-time systems [J].

Luckow, Kasper S. ;

Pasareanu, Corina S. ;

Thomsen, Bent .

EURASIP JOURNAL ON EMBEDDED SYSTEMS, 2015, 2015 (01)

[49] Quantitative Timing Analysis for Cyber-Physical Systems Using Uncertainty-Aware Scenario-Based Specifications [J].

Hu, Ming ;

Duan, Wenxue ;

Zhang, Min ;

Wei, Tongquan ;

Chen, Mingsong .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2020, 39 (11) :4006-4017

← 1 2 3 4 5 →