Intelligent Model Checking. Real-world systems are typically so complex that software engineers require specialised CAD tools to debug and verify a design. Model checking is a formal method that is used extensively for this purpose, particularly for mission-critical systems. In this work, a new kind of verifying tool, based on model checking, is developed. This new model checker is intelligent because a heuristic search is integrated into the underlying formalism. It is not exhaustive, and is mo ....Intelligent Model Checking. Real-world systems are typically so complex that software engineers require specialised CAD tools to debug and verify a design. Model checking is a formal method that is used extensively for this purpose, particularly for mission-critical systems. In this work, a new kind of verifying tool, based on model checking, is developed. This new model checker is intelligent because a heuristic search is integrated into the underlying formalism. It is not exhaustive, and is more efficient than a traditional model checker during the design phase because it does only a minimum amount of work in its search for a fault.Read moreRead less
Quality of Service-based Scheduling of e-Research Application Workflows on Global Grids. e-Research has the potential to offer Australia significant economic and social benefits as it enables researchers from different disciplines and organisations to engage in collaborative scientific investigation. In e-Research environments, users need to have secure access to remote resources owned by different organisations. Since these resources are not directly under the control of e-Research applications ....Quality of Service-based Scheduling of e-Research Application Workflows on Global Grids. e-Research has the potential to offer Australia significant economic and social benefits as it enables researchers from different disciplines and organisations to engage in collaborative scientific investigation. In e-Research environments, users need to have secure access to remote resources owned by different organisations. Since these resources are not directly under the control of e-Research applications, they need to negotiate with resource providers for access time, duration, and the level of quality of service expected to make sure that the interlinked operations are performed as required. This project develops information and communications technologies that enable the creation of such e-Research environments.Read moreRead less
Verified Emulation of Legacy Mission Computer Systems. Processor obsolescence is a serious maintenance problem for long-lived computer control systems in military aircraft and other critical applications. A promising solution is to interpose an emulator program between the original "legacy" software and a replacement processor. Unfortunately, no techniques exist for accurately verifying that this procedure preserves the original system's functional and timing behaviour. A particular challenge ....Verified Emulation of Legacy Mission Computer Systems. Processor obsolescence is a serious maintenance problem for long-lived computer control systems in military aircraft and other critical applications. A promising solution is to interpose an emulator program between the original "legacy" software and a replacement processor. Unfortunately, no techniques exist for accurately verifying that this procedure preserves the original system's functional and timing behaviour. A particular challenge is that processor emulations involve both legacy code and new subroutines, written in different programming languages. This project will enable verification of safety and mission-critical emulated systems by devising a multilingual modelling and reasoning formalism, based on program refinement theory.Read moreRead less
Metamorphic slices and their applications in fault localization. The main purpose of this project is to enhance the quality of software. The expected outcomes include the delivery of new cost-effective methods to debug software, and the extension of current debugging methods to be applicable in wider contexts.
Model-based error location in Java programs. The construction of modern software requires extensive testing and
debugging in addition to using appropriate specification, design, and
verification techniques. Testing and debugging are very time-consuming
and costly, drawing - according to recent articles - "typically 50%
or more of the resources for software projects''. By providing a new,
flexible approach to the debugging of complex software, this project
offers the potential of significant cost ....Model-based error location in Java programs. The construction of modern software requires extensive testing and
debugging in addition to using appropriate specification, design, and
verification techniques. Testing and debugging are very time-consuming
and costly, drawing - according to recent articles - "typically 50%
or more of the resources for software projects''. By providing a new,
flexible approach to the debugging of complex software, this project
offers the potential of significant cost savings, highly beneficial to
the ICT industry. Lessons learned from the demonstration prototype,
can be directly carried over into commercial tool development. In
addition, the project strengthens links to high quality European
research laboratories.Read moreRead less
Cost-effective use of assertions in the verification and validation of distributed and real-time systems. The project will reinforce Australia as a world leader in empirical software engineering and software verification and validation research, thus building on Australia's strengths in ICT research and innovation. Through the involvement of a local software verification and validation company and through industrial case studies, this project will also improve the software verification and valid ....Cost-effective use of assertions in the verification and validation of distributed and real-time systems. The project will reinforce Australia as a world leader in empirical software engineering and software verification and validation research, thus building on Australia's strengths in ICT research and innovation. Through the involvement of a local software verification and validation company and through industrial case studies, this project will also improve the software verification and validation capabilities of local industry, allow them to save software development costs, and improve the quality of the software produced.Read moreRead less
Privacy-preserving online user matching. This project aims to develop efficient techniques to preserve the privacy of users of online matching websites used for finding employment, friends and partners. The project expects to generate new knowledge in privacy preserving user matching with multiple servers. The expected outcomes are new techniques that can find matching users without revealing their interests to the matching server and a prototype based on these techniques. This should alleviate ....Privacy-preserving online user matching. This project aims to develop efficient techniques to preserve the privacy of users of online matching websites used for finding employment, friends and partners. The project expects to generate new knowledge in privacy preserving user matching with multiple servers. The expected outcomes are new techniques that can find matching users without revealing their interests to the matching server and a prototype based on these techniques. This should alleviate the privacy concerns of people using online tools that require providing personal information.Read moreRead less
Enhancing information credibility using mathematical prediction. The aim of this project is to develop theory, techniques, mathematical tools and practical algorithms for rumor detection and forecast in social media to enhance credibility of news, especially in time-sensitive situations and trending events. This project will significantly advance human knowledge of rumor formation, detection, and forecast, which will enable timely and efficient counter attacks. The outcomes from this project wil ....Enhancing information credibility using mathematical prediction. The aim of this project is to develop theory, techniques, mathematical tools and practical algorithms for rumor detection and forecast in social media to enhance credibility of news, especially in time-sensitive situations and trending events. This project will significantly advance human knowledge of rumor formation, detection, and forecast, which will enable timely and efficient counter attacks. The outcomes from this project will offer a reliable information environment for our society.Read moreRead less
Domain-specific visual languages for big data analytics applications. This project aims to invent domain-specific visual languages and support model-driven engineering based infrastructure so domain experts can specify, generate and apply complex data analytics and visualisation techniques. Many domains, including intelligent transport, business intelligence, and population health, need more effective “big data” analytics and visualisation. A challenge is to combine detailed domain knowledge – w ....Domain-specific visual languages for big data analytics applications. This project aims to invent domain-specific visual languages and support model-driven engineering based infrastructure so domain experts can specify, generate and apply complex data analytics and visualisation techniques. Many domains, including intelligent transport, business intelligence, and population health, need more effective “big data” analytics and visualisation. A challenge is to combine detailed domain knowledge – what the data means and what it can be used for – with sophisticated, scalable computational techniques to mine and present information from the huge volumes of raw data. This project is expected to improve productivity and quality of big data analytics and visualisation in critical domains.Read moreRead less
Next generation garbage collection: discovery, design, and development. This project aims to improve the performance of programming languages used by millions of Australians every day, such as Java, JavaScript and PHP by developing improved memory-management algorithms. These languages use what is referred to as “garbage collection” to ensure memory is managed without data loss, but do so conservatively and consequently cause performance challenges and energy overheads. This project expects to p ....Next generation garbage collection: discovery, design, and development. This project aims to improve the performance of programming languages used by millions of Australians every day, such as Java, JavaScript and PHP by developing improved memory-management algorithms. These languages use what is referred to as “garbage collection” to ensure memory is managed without data loss, but do so conservatively and consequently cause performance challenges and energy overheads. This project expects to provide these languages with improved memory-management algorithms, and provides researchers and industry with a framework for innovation. This project will enable safe software that is more efficient on today's hardware and able to exploit emerging hardware. This project should lead to better performance and energy savings for server applications, phones, watches, and smart appliances, while ensuring memory safety.Read moreRead less