Timing analysis of scenario-based specifications using linear programming
作者： Xuandong Li , Minxue Pan , Lei Bu , Linzhang Wang , Jianhua Zhao
DOI: 10.1002/STV.434
关键词: Sequence diagram 、 Asynchronous communication 、 Model checking 、 Linear programming 、 Unified Modeling Language 、 Static timing analysis 、 Path (graph theory) 、 Computer science 、 Theoretical computer science 、 Reachability
摘要: Scenario-based specifications (SBSs), such as UML interaction models, offer an intuitive and visual way of describing design requirements, are playing increasingly important role in the software systems. This paper presents approach to timing analysis SBSs expressed by models. The considers more general expressive constraints sequence diagrams (SDs), gives a solution reachability analysis, constraint conformance bounded delay problems, which reduces these problems into linear programs. With synchronous interpretation SD compositions, algorithms form decision procedure for class where any loop path is time-independent other parts path. These also semi-decision with both asynchronous composition semantics. supports SBSs, investigates all paths bound limit one one, performs each finite programming. A tool prototype has been developed support this approach. Copyright © 2010 John Wiley & Sons, Ltd. (This programming-based scenario-based (SBSs) diagrams, solve reachability, SBSs. loop-unlimited path, SBSs.)
acm.org
sci-hub.se 参考文章(25)
Gerard Holzmann, Spin model checker, the: primer and reference manual Addison-Wesley Professional. ,(2003)
Rajeev Alur, Gerard J. Holzmann, Doron Peled, An analyzer for message sequence charts tools and algorithms for construction and analysis of systems. pp. 35- 48 ,(1996) , 10.1007/3-540-61042-1_37
Johan Lilius, Xuandong Li, Timing analysis of UML sequence diagrams Lecture Notes in Computer Science. pp. 661- 674 ,(1999) , 10.5555/1767297.1767364
Hanêne Ben-Abdallah, Stefan Leue, Timing Constraints in Message Sequence Chart Specifications formal techniques for networked and distributed systems. pp. 91- 106 ,(1997) , 10.1007/978-0-387-35271-8_6
Gerard J. Holzmann, The SPIN Model Checker ,(2003)
Doron A. Peled, Software reliability methods Springer. ,(2001) , 10.1007/978-1-4757-3540-6
Vladimir Levin, Doron Peled, Verification of Message Sequence Charts via Template Matching colloquium on trees in algebra and programming. pp. 652- 666 ,(1997) , 10.1007/BFB0030632
Henrik Hulgaard, Steven M. Burns, Bounded Delay Timing Analysis of a Class of CSP Programs formal methods. ,vol. 11, pp. 265- 294 ,(1997) , 10.1023/A:1008655714875
Ursula Goltz, Thomas Gehrke, Michaela Huhn, Thomas Firley, Karsten Diethers, Timed sequence diagrams and tool-based analysis: a case study Lecture Notes in Computer Science. pp. 645- 660 ,(1999) , 10.5555/1767297.1767363
Rajeev Alur, Mihalis Yannakakis, Model Checking of Message Sequence Charts CONCUR’99 Concurrency Theory. pp. 114- 129 ,(1999) , 10.1007/3-540-48320-9_10