A5015799790- Formal Methods in Verification
- Software Testing and Debugging Techniques
- Software Reliability and Analysis Research
- Petri Nets in System Modeling
- Logic, programming, and type systems
- Teaching and Learning Programming
- Software Engineering Research
- Mobile Ad Hoc Networks
- Distributed systems and fault tolerance
- Model-Driven Software Engineering Techniques
- Peer-to-Peer Network Technologies
- Security and Verification in Computing
- Access Control and Trust
- Safety Systems Engineering in Autonomy
- Blockchain Technology Applications and Security
- Logic, Reasoning, and Knowledge
- Embedded Systems Design Techniques
- Cooperative Communication and Network Coding
- Real-Time Systems Scheduling
- Opportunistic and Delay-Tolerant Networks
- Advanced Software Engineering Methodologies
- Software System Performance and Reliability
- Advanced Malware Detection Techniques
- Simulation Techniques and Applications
- Open Education and E-Learning
Macquarie University
2022-2024
University of Twente
2016-2021
Scientific Methods (United States)
2020
UNSW Sydney
2005-2015
University of the South Pacific
2013-2015
Data61
2005-2012
Australian Government
2006
Australian Research Council
2006
Carnegie Mellon University
2002-2004
Radboud University Nijmegen
1998-2001
Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite space, can often be verified using ordinary model checking together with a finite-state abstraction. Model inconclusive, however, in case the abstraction must refined. This paper presents new procedure to perform this refinement operation for abstractions systems. Following approach originally developed [11, 25], constructs that eliminates counterexample generated...
Scheduling in an environment with constraints of many different types is known to be a hard problem. We tackle this problem for integrated steel plant Ghent, Belgium, using UPPAAL, model checker networks timed automata. show how translate schedulability reachability, enabling us use UPPAAL's checking algorithms.
We propose AWN (Algebra for Wireless Networks), a process algebra tailored to the modelling of Mobile Ad hoc Network (MANET) and Mesh (WMN) protocols. It combines novel treatments local broadcast, conditional unicast data structures. In this framework we present rigorous analysis On-Demand Distance Vector (AODV) protocol, popular routing protocol designed MANETs WMNs, one four protocols currently standardised by IETF MANET working group. give complete unambiguous specification thereby...
<p>This paper introduces the model of linearly priced timed automata as an extension automata, with prices on both transitions and locations. For this we consider minimum-cost reachability problem: i.e. given a automaton target<br />state, determine minimum cost executions from initial state to target state. This problem generalizes minimum-time for ordinary automata. We prove decidability by offering algorithmic solution, which is based combination branch-and-bound techniques...
Software has been under scrutiny by the verification community from various angles in recent past. There are two major algorithmic approaches to ensure correctness of and eliminate bugs such systems: software model checking static analysis. Those typically complementary. In this paper we use a approach solve analysis problems. This not only avoids scalability abstraction issues associated with checking, it allows for specifying new properties concise elegant way, scales well large code...
<p>In this paper we present an algorithm for efficiently computing<br /> the minimum cost of reaching a goal state in model Uniformly<br />Priced Timed Automata (UPTA). This can be seen as submodel<br />of recently suggested linearly priced timed automata, which<br />extends automata with prices on both locations and transitions.<br />The presented is based symbolic semantics UTPA, and<br />an efficient representation operations difference bound...