Bibliography: leaves 211-220 This thesis examines automated formal verification techniques and their associated space and time implementation complexity when applied to finite state concurrent systems. The focus is on concurrent systems expressed in the Communicating Sequential Processes (CSP) framework. An approach to the compilation of CSP system descriptions into boolean formulae in the form of Ordered Binary Decision Diagrams (OBDD) is presented, further utilised by a basic algorithm that checks a refinement or equivalence relation between a pair of processes in any of the three CSP semantic models. The performance bottlenecks of the basic refinement checking algorithms are identified and addressed with the introduction of a number of novel techniques and algorithms. Algorithms described in this thesis are implemented in the Adelaide Tefinement Checking Tool.

Bibliography: leaves 211-220 / xviii, 220 leaves : charts ; 30 cm. / Title page, contents and abstract only. The complete thesis in print form is available from the University Library. / This thesis examines automated formal verification techniques and their associated space and time implementation complexity when applied to finite state concurrent systems. The focus is on concurrent systems expressed in the Communicating Sequential Processes (CSP) framework. An approach to the compilation of CSP system descriptions into boolean formulae in the form of Ordered Binary Decision Diagrams (OBDD) is presented, further utilised by a basic algorithm that checks a refinement or equivalence relation between a pair of processes in any of the three CSP semantic models. The performance bottlenecks of the basic refinement checking algorithms are identified and addressed with the introduction of a number of novel techniques and algorithms. Algorithms described in this thesis are implemented in the Adelaide Tefinement Checking Tool. / Thesis (Ph.D.)--University of Adelaide, Dept. of Computer Science, 2002

Not available / text

Not available

Not available

Bibliography: leaves 211-220 / xviii, 220 leaves : charts ; 30 cm. / Title page, contents and abstract only. The complete thesis in print form is available from the University Library. / This thesis examines automated formal verification techniques and their associated space and time implementation complexity when applied to finite state concurrent systems. The focus is on concurrent systems expressed in the Communicating Sequential Processes (CSP) framework. An approach to the compilation of CSP system descriptions into boolean formulae in the form of Ordered Binary Decision Diagrams (OBDD) is presented, further utilised by a basic algorithm that checks a refinement or equivalence relation between a pair of processes in any of the three CSP semantic models. The performance bottlenecks of the basic refinement checking algorithms are identified and addressed with the introduction of a number of novel techniques and algorithms. Algorithms described in this thesis are implemented in the Adelaide Tefinement Checking Tool. / Thesis (Ph.D.)--University of Adelaide, Dept. of Computer Science, 2002

Program verification is vital as more and more users are creating, downloading and executing foreign computer programs. Software verification tools provide a means for determining if a program adheres to a user’s security requirements, or security policy. There are many verification tools that exist for checking different types of policies on different types of programs. Currently however, there is no verification tool capable of determining if all types of programs satisfy all types of policies. This thesis describes a framework for supporting multiple verification tools to determine program satisfaction. A user’s security requirements are represented at multiple levels of abstraction as Intermediate Execution Environments. Using a sequence of configurations, a user’s security requirements are transformed from the abstract level to the tool level, possibly for multiple verification tools. Using a number of case studies, the validity of the framework is shown.

Refactorings are structured changes to existing software that leave its externally observable behaviour unchanged. The intent is to improve readability, performance or other non-behavioural properties of a program. Agile software engineering processes stress the importance of refactoring to keep program code extensible and maintainable. Despite their apparent benefits, manual refactorings are time-consuming and prone to introducing unintended side effects. Research efforts seek to support and automate refactoring tasks to overcome these limitations. Current research in automatic refactoring, as well as state-of-the-art automated refactoring tools, frequently rely on syntax-driven approaches. They focus on transformations which can be safely performed using only syntactic information about a program or act overly conservative when knowledge about program semantics is required. In this thesis we explore semantics-driven refactoring, which enables much more sophisticated refactoring schemata. Our semantics-driven refactorings rely on formal verification algorithms to reason over a program's behaviour, and we conjecture they are more precise and can handle more complex code scenarios than syntax-driven ones. For this purpose, we present and implement a program synthesis algorithm based on the CEGIS paradigm and demonstrate that it can be applied to a diverse set of applications. Our synthesiser relies on the bounded model checker CBMC as an oracle and is based on an earlier research prototype called Kalashnikov. We further define our Java Stream Theory (JST) which allows us to reason over a set of interesting semantic refactorings. Both solutions are combined into an automated semantic refactoring decision procedure, reasoning over program behaviours, and searching the space of possible refactorings using program synthesis. We provide experimental evidence to support our conjecture that semanticsdriven refactorings exceed syntax-driven approaches in precision and scope.

Submitted by Pedro Henrique Rodrigues (pedro.henriquer@ufpe.br) on 2015-03-05T18:45:35Z No. of bitstreams: 2 jpso-master_rabbit_complete.pdf: 1450168 bytes, checksum: 081b9f94c19c494561e97105eb417001 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-05T18:45:35Z (GMT). No. of bitstreams: 2 jpso-master_rabbit_complete.pdf: 1450168 bytes, checksum: 081b9f94c19c494561e97105eb417001 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2012-08-30 / Data-races are an important kind of error in concurrent shared-memory programs. Software model checking is a popular approach to find them. This research proposes a novel approach to find races that complements model-checking by efficiently reporting precise warnings during state-space exploration (SSE): Rabbit. It uses information obtained across different paths explored during SSE to predict likely racy memory accesses. We evaluated Rabbit on 33 different scenarios of race, involving a total of 21 distinct application subjects of various sources and sizes. Results indicate that Rabbit reports race warnings very soon compared to the time the model checker detects the race (for 84.8% of the cases it reports a true warning of race in <5s) and that the warnings it reports include very few false alarms. We also observed that the model checker finds the actual race quickly when it uses a guided-search that builds on Rabbit’s output (for 74.2% of the cases it reports the race in <20s).

Routing metrics are important mechanisms to adjust routing protocols' path selection according to the needs of a network system. However, if a routing metric design does not correctly match a particular routing protocol, the protocol may not be able to find an optimal path; routing loops can be produced as well. Thus, the compatibility between routing metrics and routing protocols is increasingly significant with the widespread deployment of wired and wireless networks. However, it is usually difficult to tell whether a routing metric can be perfectly applied to a particular routing protocol. Manually enumerating all possible test cases is very challenging and often infeasible. Therefore, it is highly desirable to have an automatic solution so that one can avoid putting an incompatible combination of routing metric and protocol into use. In this thesis, the above issue has been addressed by developing two automated checking systems for examining the compatibility between real world routing metric and protocol implementations. The automatic routing protocol checking system assumes that some properties of routing metrics are given and the system's job is to check if a new routing protocol is able to achieve optimal, consistent and loop- free routing when it is combined with metrics that hold the given metric properties. In contrast to the protocol checking system, the automatic routing metric checking system assumes that a routing protocol is given and the checking system needs to verify if a new metric implementation will be able to work with this protocol. Experiments have been conducted to verify the correctness of both protocol and metric checking systems. / Master of Science