Font Size: a A A

Research On Timing Analysis Of Scenario-based Specifications

Posted on:2015-01-04Degree:DoctorType:Dissertation
Country:ChinaCandidate:M X PanFull Text:PDF
GTID:1318330491963511Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
As the application of computer technology becomes wider and deeper,the scales and complexities of software systems grow increasingly larger.The interactions and timing constraints have become important aspects of software requirements and designs.As an effect and visual approach to describing system interactions,scenario-based speci-fications(SBS)have already been widely used in industry.Currently,the mainstream descriptive languages for SBS,including message se-quence charts(MSC)and the Unified Modeling Language(UML)interaction models,only provide simple mechanisms for describing timing constraints,which cannot meet the need to describe complex timing constraints.In practical applications,systems are typically composed of multiple scenarios.The interpretation of scenario composition can be synchronous or asynchronous.For SBS with synchronous concatenation,their timing analysis problems are often transformed to time automata's analysis problems,whose complexity can be difficult to control;For SBS with asynchronous concatena-tion,the timing analysis problems are generally undecidable.This work studies the timing analysis problems of SBS composed of multiple s-cenarios.For SBS with synchronous concatenation,we propose to encode SBS direct-ly and reduce the timing analysis problems to linear programming problems.Based on this approach,the analysis complexity is controlled effectively.For the undecid-able timing analysis problems of SBS with asynchronous concatenation,we identified a new decidable subclass named flexible loop-closed SBS,and solved the reachability analysis and the bounded delay analysis problems.The main contributions of this work address the following aspects:To meet the need of timing analysis of SBS,we give the formal semantics for S-BS,especially the formal definitions of SBS' timed behavior under synchronous composition and asynchronous composition.In the mean time we extend the tim-ing descriptive mechanisms in SBS,which enables the description of the com-plex relations among multiple time separations between events.For SBS with synchronous concatenation,we propose an approach to encoding the SBS directly,and therefore transforming the timing analysis problems to linear programming problems,which then are efficiently solved by mature linear programming algorithms.In this way,we make the complexity of the analysis problems in control.Based on this approach,for a class of SBS named loop-unlimited SBS,we solved the reachability analysis,the constraint conformance analysis and the bounded delay analysis problems.For SBS with asynchronous concatenation,we identified a new decidable class named flexible loop-closed SBS.This class does not restrict the structures of SBS,and only makes restrictions to the timing constraints.We solved the reachability analysis and the bound delay analysis problems for flexible loop-closed SBS.We propose a path-oriented bounded timing analysis approach for SBS.Based on transforming the bounded timing analysis problems of a single path to linear programs,this approach uses an optimized depth-first search to traverse and ana?lyze all the path in the SBS within a given threshold.With this approach,we can control the complexity of bounded timing analysis of SBS.Based on the above work,we implemented a tool called TASS:Timing Analyzer of Scenario-based Specifications.TASS consists of a friendly GUI to create and modify SBS,and implements all the timing analysis functions of SBS.The experiments show that on real-world systems' SBS,TASS has good performance and scalability.
Keywords/Search Tags:Scenario-based Specifications, UML Interaction Models, Message Se-quence Charts, Timing Analysis, Bounded Model Checking, Scenario-based Specifi-cations with Asynchronous Concatenation
PDF Full Text Request
Related items