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 条

[21] Model checking temporal metric specifications with Trio2Promela [J].

Bianculli, Domenico ;

Spoletini, Paola ;

Morzenti, Angelo ;

Pradella, Matteo ;

Pietro, Pierluigi San .

INTERNATIONAL SYMPOSIUM ON FUNDAMENTALS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4767 :388-+

[22] Spatiotemporal model checking of location and mobility related security policy specifications [J].

Unal, Devrim ;

Caglayan, Mehmet Ufuk .

TURKISH JOURNAL OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCES, 2013, 21 (01) :144-173

[23] Using abstraction and model checking to detect safety violations in requirements specifications [J].

Heitmeyer, C ;

Kirby, J ;

Labaw, B ;

Archer, M ;

Bharadwaj, R .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (11) :927-948

[24] Automatic Verification of Behavior of UML Requirements Specifications using Model Checking [J].

Matsuura, Saeko ;

Ikeda, Sae ;

Yokotae, Kasumi .

PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT (MODELSWARD), 2020, :158-166

[25] Constraint-based deadlock checking of high-level specifications [J].

Hallerstede, Stefan ;

Leuschel, Michael .

THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2011, 11 :767-782

[26] Towards model checking executable UML specifications in mCRL2 [J].

Hansen, Helle Hvid ;

Ketema, Jeroen ;

Luttik, Bas ;

Mousavi, MohammadReza ;

van de Pol, Jaco .

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) :83-90

[27] Checking conformance for time-constrained scenario-based specifications [J].

Akshay, S. ;

Gastin, Paul ;

Mukund, Madhavan ;

Kumar, K. Narayan .

THEORETICAL COMPUTER SCIENCE, 2015, 594 :24-43

[28] Practical Behavioral Inconsistency Detection between Source Code and Specification using Model Checking [J].

Matsuura, Saeko ;

Aoki, Yoshitaka ;

Ogata, Shinpei .

2014 IEEE INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING WORKSHOPS (ISSREW), 2014, :124-125

[29] Checking Multi-Agent Systems against Temporal-Epistemic Specifications [J].

Chen, Ran ;

Zhang, Wenhui .

2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, :21-30

[30] The Electrum Analyzer: Model Checking Relational First-Order Temporal Specifications [J].

Brunel, Julien ;

Chemouil, David ;

Cunha, Alcino ;

Macedo, Nuno .

PROCEEDINGS OF THE 2018 33RD IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMTED SOFTWARE ENGINEERING (ASE' 18), 2018, :884-887

← 1 2 3 4 5 →