A5006104972- Formal Methods in Verification
- Distributed systems and fault tolerance
- Advanced Software Engineering Methodologies
- Model-Driven Software Engineering Techniques
- Logic, programming, and type systems
- Parallel Computing and Optimization Techniques
- Security and Verification in Computing
- Software Testing and Debugging Techniques
- Real-Time Systems Scheduling
- Software Reliability and Analysis Research
- Multi-Agent Systems and Negotiation
- Software Engineering Research
- Embedded Systems Design Techniques
- Service-Oriented Architecture and Web Services
- Petri Nets in System Modeling
- Logic, Reasoning, and Knowledge
- Manufacturing Process and Optimization
- Modular Robots and Swarm Intelligence
- Business Process Modeling and Analysis
- Advanced Database Systems and Queries
- Radiation Effects in Electronics
- Simulation Techniques and Applications
- Advanced Memory and Neural Computing
- AI-based Problem Solving and Planning
- Advanced Malware Detection Techniques
The University of Queensland
2015-2024
Defence Science and Technology Group
2010-2024
Queensland University of Technology
2014-2023
University of Cambridge
2009-2013
University of Kent
2009
Technische Universität Berlin
1997-2002
Software (Spain)
2000
University of Manchester
1997
Institut national de recherche en informatique et en automatique
1994
Centre National de la Recherche Scientifique
1994
Formal Methods (FMs) radically improve the quality of code artefacts they help to produce. They are simple, probably accessible first-year undergraduate students and certainly second-year beyond. Nevertheless, in many cases, not part a general recommendation for course curricula, i.e., taught — yet valuable. One reason this is that teaching “Formal Methods” often confused with logic theory. This article advocates what we call FM thinking : application ideas from applied informal,...
The formal development of large or complex systems can often be facilitated by the use more than one specification language. Such a combination languages is particularly suited to concurrent distributed systems, where both modelling processes and state necessary. This paper presents an approach refinement verification specifications written using Object-Z CSP (communicating sequential processes). A common semantic basis for two enables unified method used, based upon refinement. To enable...
This paper investigates model checking Object-Z classes via their translation to the input notation of CSP checker FDR. Such a must not only be concerned with preserving semantics original specification, but also how efficiently resulting specification can checked. Hence, alternative schemes and compares specifications
Correctness of concurrent objects is defined in terms conditions that determine allowable relationships between histories a object and those the corresponding sequential object. Numerous correctness have been proposed over years, more recently as algorithms implementing adapted to cope with multicore processors relaxed memory architectures. We present formal framework for defining architectures, covering both standard totally ordered newer memory, which allows them be expressed uniform...