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 条

[31] Descartes-Agent: Verifying Formal Specifications Using the Model Checking Technique [J].

Subburaj, Vinitha Hannah ;

Urban, Joseph E. .

2018 SECOND IEEE INTERNATIONAL CONFERENCE ON ROBOTIC COMPUTING (IRC), 2018, :392-398

[32] Isomorph-free model enumeration: A new method for checking relational specifications [J].

Jackson, D ;

Jha, S ;

Damon, CA .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (02) :302-343

[33] Model Checking of Location and Mobility Related Security Policy Specifications in Ambient Calculus [J].

Unal, Devrim ;

Akar, Ozan ;

Caglayan, M. Ufuk .

COMPUTER NETWORK SECURITY, 2010, 6258 :155-168

[34] Generating test case specifications of web service composition using model checking [J].

钱铃莉 ;

陈怡海 .

Advances in Manufacturing, 2011, (05) :409-414

[35] Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications [J].

Kong, Jeremy ;

Lomuscio, Alessio .

AAMAS'17: PROCEEDINGS OF THE 16TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS, 2017, :114-122

[36] Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces [J].

Kong, Jeremy ;

Lomuscio, Alessio .

PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS (AAMAS' 18), 2018, :166-174

[37] Timing analysis of scenario-based specifications using linear programming [J].

Li, Xuandong ;

Pan, Minxue ;

Bu, Lei ;

Wang, Linzhang ;

Zhao, Jianhua .

SOFTWARE TESTING VERIFICATION & RELIABILITY, 2012, 22 (02) :121-143

[38] MODEL CHECKING OF CONTINUOUS-TIME MARKOV CHAINS AGAINST TIMED AUTOMATA SPECIFICATIONS [J].

Chen, Taolue ;

Han, Tingting ;

Katoen, Joost-Pieter ;

Mereacre, Alexandru .

LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (01)

[39] Using Model-Checking for Timing Verification in Industrial System Design [J].

Rioux, Laurent ;

Henia, Rafik ;

Sordon, Nicolas .

10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION WORKSHOPS - ICSTW 2017, 2017, :377-378

[40] SAT and LP Collaborative Bounded Timing Analysis of Scenario-Based Specifications [J].

Lu, Longlong ;

Yang, Wenhua ;

Pan, Minxue ;

Zhang, Tian .

THE 12TH ASIA-PACIFIC SYMPOSIUM ON INTERNETWARE, INTERNETWARE 2020, 2021, :229-239

← 1 2 3 4 5 →