Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 16 of 16 for “"State-space Explosion"”.
-
On the formal verification of ATM switches
… and sequential equivalence checking is the state space explosion. Another drawback of model checking is lack of methods on establishing an environment and expressing a property. In this thesis, we propose Property Division techniques which avoid the state space explosion problem by deducing …
-
On Improving Backwards Reasoning with Symbolic Execution: Integrating Loop Summarization, Alias Analysis, and Compositional Summarization
… execution faces a fundamental challenge known as state-space explosion, where the number of potential execution paths grows exponentially. While backwards symbolic execution (BSE) offers some advantages over forward approaches in managing this explosion, it still struggles with path explosion when …
-
Improved Symbolic Model Checking of Real-Time Systems
… that current techniques still encounter the state space explosion problem. The aim of this thesis is to study the symbolic model checking problems of real-time systems and to explore techniques to mitigate the state space explosion problem. In the literature, the model checking technique …
-
Improvements on handling design errors in communication protocols.
… in communication protocols include deadlock states, unspecified receptions, channel overflow, non-executable transitions, etc. Such design errors can be removed via protocol synthesis, or be detected through reachability analysis. The former may introduce more states and transitions than …
-
A practical model checking approach using FormalCheck
… automatic formal verification is limited by the state explosion problem. This thesis presents a practical verification approach using FormalCheck, which helps reducing the state space explosion problem when verifying the high level descriptions of practical systems. This approach relies on the …
-
Scalable attack modelling in support of security information and event management
… network. Nodes in an attack graph represent the state of a network at a point in time while arcs between nodes indicate the transformation of a network from one state to another, via the exploit of a vulnerability. Using attack graphs allows system and network configuration information to be …
-
Functionally Encapsulated Modules: A Computer Aided Software Engineering Methodology for the Implementation of Computer Integrated Manufacturing
… the functional modelling power of Petri nets. State space explosion is reduced as Petri nets are used only for modelling the functionality of objects. However, the modules also retain the abilities of simulation tool and mathematical proof of the original Petri net. The methodology and …
-
Bounded Aggregation Techniques to Solve Large Markov Models
… Markovian modeling is limited by the ""state-space explosion,"" or the exponential growth of the state space of a Markovian model as detail is added to the model. It is our thesis that aggregation techniques can be used to solve, at an acceptable level of accuracy, Markovian models that …
-
Automatic techniques for detecting and exploiting symmetry in model checking
… of model checking is limited due to the state-space explosion problem – as the number of components represented by a model increase, the worst case size of the associated state-space grows exponentially. Current techniques can handle limited kinds of symmetry, e.g. full symmetry between …
-
Trace analysis of protocols based on formal concurrent specifications
… which is based on single module extended finite state machines, handles both control and data flows for single module specifications. Symbolic evaluation is used to detect and delete infeasible paths that may be generated. Practical considerations which may occur in a real test environment, such …
-
Low complexity system architecture design for medical Cyber-Physical-Human Systems (CPHS)
… the verification cost, which is known as state space explosion problems. We propose two architectural patterns: Interruptible Remote Procedure Call (RPC) and Consistent View Generation and Coordination (CVGC) protocol to properly handle asynchronous communication and exceptions with low …
-
Exploring Hybrid Dynamic and Static Techniques for Software Verification
… of error detection in software testing and the state space explosion problem in software formal verification (model checking). In this dissertation, we investigate several hybrid techniques that explore dynamic (with program execution), static (without program execution) as well as the synergies …
-
Attacking complexity in logic synthesis of asynchronous circuits
… approach to tackle complexity problems like state space explosion in logic synthesis of SI circuits. The (structural) decomposition of STGs is guided by a partition of the output signals and generates a usually much smaller component STG for each partition member, i.e. a component STG with a …
-
I/O-Automata based formal approach to Web Services Choreography
… behaviors. Such a technique is subject to state-space explosion. In light of this, we have developed a tabled logic programming technique which generates and explores compositions in a goal-directed fashion to prove/disprove the existence of choreographer and to infer whether the desired …
-
Pragmatic approach to the development of robust real-time protocols
… for Petri net based techniques is that of state space explosion, a modular approach to both the design and analysis would help cope with this problem. Although extensions to Petri nets that allow module construction exist, generally the modularisation is restricted to the specification, and …
-
Effective Approaches to Abstraction Refinement for Automatic Software Verification
… for automatic software verification that tracks state information concretely. From a thorough evaluation based on well over 4 000 verification tasks from the latest edition of the International Competition on Software Verification (SV-COMP), we learn that this plain value analysis leads to an …