Timing analysis of scenario-based specifications using linear programming

被引:0
|
作者
Li, Xuandong [1 ,2 ]
Pan, Minxue [1 ,2 ]
Bu, Lei [1 ,2 ]
Wang, Linzhang [1 ,2 ]
Zhao, Jianhua [1 ,2 ]
机构
[1] Nanjing Univ, Dept Comp Sci & Technol, Nanjing 210093, Jiangsu, Peoples R China
[2] Nanjing Univ, State Key Lab Novel Software Technol, Nanjing 210093, Jiangsu, Peoples R China
来源
基金
中国国家自然科学基金;
关键词
real-time systems; software verification; model checking; UML interaction models; bounded delay analysis; ANALYZER;
D O I
10.1002/stv.434
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Scenario-based specifications (SBSs), such as UML interaction models, offer an intuitive and visual way of describing design requirements, and are playing an increasingly important role in the design of software systems. This paper presents an approach to timing analysis of SBSs expressed by UML interaction models. The approach considers more general and expressive timing constraints in UML sequence diagrams (SDs), and gives a solution to the reachability analysis, constraint conformance analysis and bounded delay analysis problems, which reduces these problems into linear programs. With the synchronous interpretation of the SD compositions, the timing analysis algorithms in the approach form a decision procedure for a class of SBSs where any loop in any path is time-independent of the other parts in the path. These algorithms are also a semi-decision procedure for general SBSs with both the synchronous and asynchronous composition semantics. The approach also supports bounded timing analysis of SBSs, which investigates all the paths in the bound limit one by one, and performs the timing analysis for each finite path by linear programming. A tool prototype has been developed to support this approach. Copyright (C) 2010 John Wiley & Sons, Ltd.
引用
收藏
页码:121 / 143
页数:23
相关论文
共 50 条
  • [1] TASS: Timing Analyzer of Scenario-Based Specifications
    Pan, Minxue
    Bu, Lei
    Li, Xuandong
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2009, 5643 : 689 - 695
  • [2] SAT and LP Collaborative Bounded Timing Analysis of Scenario-Based Specifications
    Lu, Longlong
    Yang, Wenhua
    Pan, Minxue
    Zhang, Tian
    [J]. THE 12TH ASIA-PACIFIC SYMPOSIUM ON INTERNETWARE, INTERNETWARE 2020, 2021, : 229 - 239
  • [3] Verifying compositional designs for scenario-based timing specifications
    Li, XD
    Zhao, JH
    Gong, JY
    Shi, YX
    Zheng, GL
    [J]. SEVENTH IEEE INTERNATIONAL SYMPOSIUM ON OBJECT-ORIENTED REAL-TIME DISTRIBUTED COMPUTING, PROCEEDINGS, 2004, : 253 - 256
  • [4] Semantically Configurable Analysis of Scenario-Based Specifications
    Cohen, Barak
    Maoz, Shahar
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2014, 2014, 8411 : 185 - 199
  • [5] Verification of Scenario-based Specifications using Templates
    Palshikar, Girish Keshav
    Bhaduri, Purandar
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 118 : 37 - 55
  • [6] Improving timing analysis effectiveness for scenario-based specifications by combining SAT and LP techniques
    Lu, Longlong
    Pan, Minxue
    Zhang, Tian
    Li, Xuandong
    [J]. SOFTWARE AND SYSTEMS MODELING, 2022, 21 (04): : 1321 - 1338
  • [7] Improving timing analysis effectiveness for scenario-based specifications by combining SAT and LP techniques
    Longlong Lu
    Minxue Pan
    Tian Zhang
    Xuandong Li
    [J]. Software and Systems Modeling, 2022, 21 : 1321 - 1338
  • [8] Quantitative Timing Analysis for Cyber-Physical Systems Using Uncertainty-Aware Scenario-Based Specifications
    Hu, Ming
    Duan, Wenxue
    Zhang, Min
    Wei, Tongquan
    Chen, Mingsong
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2020, 39 (11) : 4006 - 4017
  • [9] Scenario-Based Methods for Interval Linear Programming Problems
    Cao, M. F.
    Huang, G. H.
    [J]. JOURNAL OF ENVIRONMENTAL INFORMATICS, 2011, 17 (02) : 65 - 74
  • [10] Checking component-based embedded software designs for scenario-based timing specifications
    Hu, J
    Yu, XF
    Zhang, Y
    Zhang, T
    Li, XD
    Zheng, GL
    [J]. EMBEDDED AND UBIQUITOUS COMPUTING - EUC 2005, 2005, 3824 : 395 - 404