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
A Compositional Model for Verifying and Programming Ecologies of Smart Internet Devices. Emerging in 21st century computing is what we perceive as device ecologies, or collections of devices that can exhibit smart behaviour, automate tasks, interact synergistically with one another, with users and Internet resources, and provide aid and value in daily life and work. Device ecologies will be seen in areas as diverse as e-commerce, health care, home automation, office automation, manufacturing, an ....A Compositional Model for Verifying and Programming Ecologies of Smart Internet Devices. Emerging in 21st century computing is what we perceive as device ecologies, or collections of devices that can exhibit smart behaviour, automate tasks, interact synergistically with one another, with users and Internet resources, and provide aid and value in daily life and work. Device ecologies will be seen in areas as diverse as e-commerce, health care, home automation, office automation, manufacturing, and defense. This project will develop a novel model and language for analyzing and programming device ecologies. This will be an Australian contribution towards techniques for constructing advanced applications that work over the computing infrastructure of the future.Read moreRead less
Early detection of component incompatibility in time-dependent computer architectures. Complex real-time systems are increasingly being built by integrating off-the-shelf components. There are obvious benefits to this approach, but the hidden costs associated with integration are still a major problem. Our proposed approach will enable early detection of integration problems, and thus provide potential for large cost savings. This brings with it clear benefits to industry. One industry that woul ....Early detection of component incompatibility in time-dependent computer architectures. Complex real-time systems are increasingly being built by integrating off-the-shelf components. There are obvious benefits to this approach, but the hidden costs associated with integration are still a major problem. Our proposed approach will enable early detection of integration problems, and thus provide potential for large cost savings. This brings with it clear benefits to industry. One industry that would benefit by such technology is the Australian Navy, which is increasingly being confronted with the challenge of integrating off-the-shelf components in large Naval Combat Systems. Read moreRead less
Simulation and verification of system-level specifications of requirements and constraints using Rosetta. Modern computer-based systems comprise a mixture of electronic hardware and embedded computer software that interacts with mechanical and other non-electrical subsystems. Future design capability will depend on being able to model the requirements and constraints of heterogeneous systems, so that they can be simulated and formally verified before being manufactured and deployed. This project ....Simulation and verification of system-level specifications of requirements and constraints using Rosetta. Modern computer-based systems comprise a mixture of electronic hardware and embedded computer software that interacts with mechanical and other non-electrical subsystems. Future design capability will depend on being able to model the requirements and constraints of heterogeneous systems, so that they can be simulated and formally verified before being manufactured and deployed. This project will develop techniques and software tools for simulation and verification based on the new Rosetta system-level design language. These tools will make the design of complex computer-based systems faster, more reliable and less costly by minimizing design errors early in the design flow.Read moreRead less
Security for Web Services. Web services, an emerging distributed computing paradigm, poses challenging problems in security, due to their dynamic decentralised scalable nature, operating over an untrusted Internet, for which no adequate solutions exist today. This research addresses the model, architecture and design of secure authorisation for web services. It achieves conceptual advances in terms of a flexible authorisation model, proposes a new XML based policy language, develops a comprehens ....Security for Web Services. Web services, an emerging distributed computing paradigm, poses challenging problems in security, due to their dynamic decentralised scalable nature, operating over an untrusted Internet, for which no adequate solutions exist today. This research addresses the model, architecture and design of secure authorisation for web services. It achieves conceptual advances in terms of a flexible authorisation model, proposes a new XML based policy language, develops a comprehensive security policy management framework, designs a distributed authorisation service and demonstrates a practical secure web service system in .NET.It presents a new approach to formally reasoning about conflict resolution policies with dynamic delegation.Read moreRead less
Integrating Model Checking and Knowledge Dynamics for System Verification. The task of system verification is to ensure the correctness of system design and specification in some automatic way. The aim of this project is to develop a new methodology and technology for computer software system verification by integrating traditional model checking approach and knowledge dynamics modeling. By deriving the results of this project, we will understand how model checking and knowledge dynamics modelin ....Integrating Model Checking and Knowledge Dynamics for System Verification. The task of system verification is to ensure the correctness of system design and specification in some automatic way. The aim of this project is to develop a new methodology and technology for computer software system verification by integrating traditional model checking approach and knowledge dynamics modeling. By deriving the results of this project, we will understand how model checking and knowledge dynamics modeling can be integrated for more effective software verification and modification, which will significantly improve current software design and development procedures, increase the correctness and stability of software systems, and provide high security for e-Commerce transaction systems.Read moreRead less
Model Update with Localisation, Constraints and Abstraction. This project will fundamentally provide a new paradigm and a system prototype for advanced computer aided system modification. It will significantly enhance Australia's leading role in the cutting edge research in computer aided system development. By applying the new methodology and technology, Australian IT industry will significantly improve its capacity for developing highly complex hardware and software systems for various applica ....Model Update with Localisation, Constraints and Abstraction. This project will fundamentally provide a new paradigm and a system prototype for advanced computer aided system modification. It will significantly enhance Australia's leading role in the cutting edge research in computer aided system development. By applying the new methodology and technology, Australian IT industry will significantly improve its capacity for developing highly complex hardware and software systems for various applications. With a strong research program across different areas such as knowledge system update, model checking and software development, and a collaborative research training environment, this project will strengthen Australia's international reputation as a leader in computing and IT research.Read moreRead less
Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap ....Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap between the informal requirements and the starting point of formally verifiable development. To minimise this gap, we develop a particularly expressive specification language, a calculus for stepwise refinement from such specifications down to distributed systems, and an automated tool for checking and supporting refinement steps in the calculus.Read moreRead less
RichProlog, a System for Deducing, Inducing and Learning in the Declarative Programming Paradigm. The aim of the project is to contribute to bridge the gap between learning and logic, theoretically and practically. Our purpose is to extend considerably the scope of the declarative programming paradigm, and build a system that can be used to solve learning or discovery problems as encountered in Artificial Intelligence. The system will enable rapid prototyping when applied to problems involving d ....RichProlog, a System for Deducing, Inducing and Learning in the Declarative Programming Paradigm. The aim of the project is to contribute to bridge the gap between learning and logic, theoretically and practically. Our purpose is to extend considerably the scope of the declarative programming paradigm, and build a system that can be used to solve learning or discovery problems as encountered in Artificial Intelligence. The system will enable rapid prototyping when applied to problems involving deduction, induction, and nonmonotonic reasoning. We intend the system to become a standard tool for tackling a broad range of applications, and the underlying theory to provide new insights on the logical foundations of Artificial Intelligence.
Read moreRead less
Model Checking Knowledge and Probability in Pursuit-Evasion Games. The research will produce software enabling modellers to better understand their models in applications including planning under uncertainty, information flow security and systems fault diagnosis. The application studied in this project is military search and rescue mission planning, resulting in greater confidence in mission success. The research is also relevant to emergency response and collision avoidance. The project will ....Model Checking Knowledge and Probability in Pursuit-Evasion Games. The research will produce software enabling modellers to better understand their models in applications including planning under uncertainty, information flow security and systems fault diagnosis. The application studied in this project is military search and rescue mission planning, resulting in greater confidence in mission success. The research is also relevant to emergency response and collision avoidance. The project will support retention of Australian intellectual property with potential for future commercialisation. It will foster linkages between Australian researchers and an international defence alliance partner. Outcomes will be available to Australian Defence through existing Defence research sharing arrangements.Read moreRead less