Global ETD Search

1	Groups of symmetries on concurrent systems West, Samantha January 2002 (has links) A well known problem when reasoning about concurrent systems is that of state explosion. One of the strategies that has been proposed to alleviate this problem is to make use of the symmetries which a concurrent system may exhibit to construct a symmetry-reduced model that reflects the behaviour of the system. The main contribution of this thesis is an investigation into the theoretical foundations of the method by considering symmetries in the context of category theory. It seems natural to do so since the morphisms that characterise each category may be thought of as a kind of simulation of behaviour. A new category of language systems is presented, together with several subcategories. Morphisms in this category are defined to preserve structure. The notion of a symmetry of a language system is defined and the quotient structure of the language system is given. The important question of behaviour preservation between the system and its symmetry-reduced model is generalised to the notion of morphism in the category. The conditions required on the morphism to ensure that it preserves behaviour are identified. These results are extended to the projection morphism that define the symmetry-reduced model by constructing a split morphism. Two specific behaviours, namely absence of deadlock and extensibility, are considered. The second contribution of this thesis is to establish a categorical relationship between the language system model and elementary nets. A vector language semantics for elementary nets is given. Functors between these categories are defined and the existence of an adjunction is proved. 005 State explosion
2	Automated Validation of User Equipment Connection States Qudus, Abdul January 2014 (has links) Telecom today has become an essence of life. Everywhere we see people using their smart phones for calling, checking email or accessing internet. To handle all these kinds of services without any intrusion is a very challenging task. This study deals with software testing which helps to ensure the quality of service to the end user. Software testing is an essential part in the software development process. Software development for telecom domain might not look as safety critical as of an airplane or nuclear reactor but it is arguably more complex. The main focus of this study is to provide automation to the unit testing of different types of radio connections that can be assigned to the end user based on the requested service and capacity of the 3G network. This research is sponsored by Ericsson to improve the testing of User Equipment Radio Connection Handling system that controls multiple possible radio connection configurations. This research attempts to identify and test all possible transitions between radio connection states. This will improve the existing manual state testing system, where changes in connection states cause dramatic impacts on test fixtures. As a solution, an automatic test case executor is proposed that generates possible transitions, which are later executed and verified automatically. testing state machine automated testing state explosion data driven testing
3	Slice—n—Dice Algorithm Implementation in JPF Noonan, Eric S. 01 July 2014 (has links) (PDF) This work deals with evaluating the effectiveness of a new verification algorithm called slice--n--dice. In order to evaluate the effectiveness of slice--n--dice, a vector clock POR was implemented to compare it against. The first paper contained in this work was published in ACM SIGSOFT Software Engineering Notes and discusses the implementation of the vector clock POR. The results of this paper show the vector clock POR performing better than the POR in Java Pathfinder by at least a factor of two. The second paper discusses the implementation of slice--n--dice and compares it against other verification techniques. The results show that slice--n--dice performs better than the other verification methods in terms of states explored and runtime when there is no error in the program or little thread interaction is needed in order for the error to manifest. state explosion partial order reduction slicing and dicing Computer Sciences
4	On-the-Fly Dynamic Dead Variable Analysis Self, Joel P. 22 March 2007 (has links) (PDF) State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space. Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism. model checking computer science static static analysis dynamic analysis analysis program program analysis Estes GDB dead variable analysis dead variable live variable live variable analysis CFG abstraction data abstraction on-the-fly static program analysis control flow graph software model checking state space depth first search state explosion state explosion problem Computer Sciences

1

Page generated in 0.1011 seconds