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
Designing for Reliability and Maintainability in Service-Oriented Architectures. This project aims to build expertise in the design of computer software, especially enterprise systems in domains such as finance and logistics that are vast in scale and highly complex and geographically separated. By fostering and formalising techniques for improving developer productivity and the reliability and maintainability of enterprise systems, Australia can secure a place as a world leader in software meth ....Designing for Reliability and Maintainability in Service-Oriented Architectures. This project aims to build expertise in the design of computer software, especially enterprise systems in domains such as finance and logistics that are vast in scale and highly complex and geographically separated. By fostering and formalising techniques for improving developer productivity and the reliability and maintainability of enterprise systems, Australia can secure a place as a world leader in software methodology, with an emphasis on technology production rather than consumption. Australian computer consulting services are a $19.5b industry, whilst the wider services sector, which is increasingly reliant on automation to stay competitive, accounts for 70% of Australia's GNP.Read moreRead less
Implementing Feferman-Landin Logic. The objective of this project is to utilise computer based verification tools (such as PVS and Rewritting Logic) to develop a software engineering environment for specifying and verifying systems written in high-level programming languages such as Java, Scheme, and ML. The project will thus subtantially advance the use of formal computer based tools to develop reliable programs and specifications for life-critical systems. The project will also develop form ....Implementing Feferman-Landin Logic. The objective of this project is to utilise computer based verification tools (such as PVS and Rewritting Logic) to develop a software engineering environment for specifying and verifying systems written in high-level programming languages such as Java, Scheme, and ML. The project will thus subtantially advance the use of formal computer based tools to develop reliable programs and specifications for life-critical systems. The project will also develop formally
based interoperability between the PVS and Maude systems, two widely
used computer tools for reasoning about complex systems.Read moreRead less
Special Research Initiatives - Grant ID: SR0566976
Funder
Australian Research Council
Funding Amount
$50,000.00
Summary
eScience and Climate: Using Grid technology to build capacity in studies of Australian climate variability. Australia possesses capability in the area of palaeoclimate modelling, but efforts to understand our past natural climate variations are hampered by the computational profligacy of such models. Further, Australia does not possess a capability in intermediate complexity models which would allow experiments that take account of tectonic time scales. This initiative aims to develop a framewor ....eScience and Climate: Using Grid technology to build capacity in studies of Australian climate variability. Australia possesses capability in the area of palaeoclimate modelling, but efforts to understand our past natural climate variations are hampered by the computational profligacy of such models. Further, Australia does not possess a capability in intermediate complexity models which would allow experiments that take account of tectonic time scales. This initiative aims to develop a framework to allow the integration of climate system models with grid computing approaches (such as Nimrod/G) and test this framework on a pilot study of the Australian palaeomonsoon system. In addition, we will use this initiative to develop international linkages to enhance our ability to address problems of importance to Australian natural climate variability.Read moreRead less
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
Integrating and automating testing in multi-agent system development. This research will provide mechanisms that facilitate easier and more thorough testing of multi-agent systems. Multi-agent technology is extremely powerful and can save businesses substantial time and effort in developing complex systems. Automated testing will ensure that systems built using this technology are more robust, and will also enable substantial savings in time required for testing. Multi agent systems are notorio ....Integrating and automating testing in multi-agent system development. This research will provide mechanisms that facilitate easier and more thorough testing of multi-agent systems. Multi-agent technology is extremely powerful and can save businesses substantial time and effort in developing complex systems. Automated testing will ensure that systems built using this technology are more robust, and will also enable substantial savings in time required for testing. Multi agent systems are notoriously difficult to test, due to their complexity. However the approaches used in this project will enable intelligent generation of test cases that are potentially difficult, and also generation of test cases that are based on specified functionality.Read moreRead less
Redesigning Typesetting for the Digital Age: Multilingual Layout on Multiple Media. We propose to create and develop a new model for character-level automatic typesetting, much more flexible than existing approaches. This model will support quality typesetting of all of the modern - and many ancient - languages and scripts, on media such as paper, computer screen, paper maps and online maps, for regular and safety-critical applications.
The fundamental innovations in this proposal are the us ....Redesigning Typesetting for the Digital Age: Multilingual Layout on Multiple Media. We propose to create and develop a new model for character-level automatic typesetting, much more flexible than existing approaches. This model will support quality typesetting of all of the modern - and many ancient - languages and scripts, on media such as paper, computer screen, paper maps and online maps, for regular and safety-critical applications.
The fundamental innovations in this proposal are the use of a tree-structured parameter space (generalization of Unix environment variables) and a multiple-pass approach to typesetting (as used in compilers). These innovative techniques will be integrated into computer software used worldwide.Read moreRead less
GriddLeS: Building Grid Applications from Legacy Software. Grid computing is emerging as a major new capability for modern, high performance technical computing. Such Grids couple geographically distributed resources such as high performance computers, workstations, clusters, and scientific instruments. Traditional methods of producing software for Grids are inefficient and error prone, and will not allow the rapid deployment of new applications. This project concerns the development of a tool t ....GriddLeS: Building Grid Applications from Legacy Software. Grid computing is emerging as a major new capability for modern, high performance technical computing. Such Grids couple geographically distributed resources such as high performance computers, workstations, clusters, and scientific instruments. Traditional methods of producing software for Grids are inefficient and error prone, and will not allow the rapid deployment of new applications. This project concerns the development of a tool that will facilitate the construction of complex Grid application using legacy software components. It will test the new ideas with a range of scientific demonstrators, including atmospheric science, geo-science and mechanical engineering.Read moreRead less
A scalable debugging framework for petascale computers. Supercomputing underpins a wide range of areas of importance to the Australian economy; mining, agriculture, engineering, medical research and pharmaceutical development to name a few. It is of critical importance that software solutions in these areas behave correctly and do not generate erroneous results. This project will develop software tools and techniques that make it possible to detect and locate errors as software is converted to r ....A scalable debugging framework for petascale computers. Supercomputing underpins a wide range of areas of importance to the Australian economy; mining, agriculture, engineering, medical research and pharmaceutical development to name a few. It is of critical importance that software solutions in these areas behave correctly and do not generate erroneous results. This project will develop software tools and techniques that make it possible to detect and locate errors as software is converted to run on the next generation of 'petascale' supercomputers. We will deploy the tools both commercially through our industry partner, and also on national high performance computing facilities.Read moreRead less