FORMAL SPECIFICATION AND VERIFICATION
Our research concentrates on automata-centric modelling of
complex systems, and the analysis of systems via automated checking
techniques. The group makes use of several different modelling
formalisms; principly the CIRCAL process algebra and Timed Automata. The
group is also engaged in the development of new formalisms based on
ideas from cellular automata and mobile agent systems to enable the
modelling of new classes of spatial concurrent systems.
Projects
-
Combining modal logics for dynamic and multi-agent systems
Modern computer software systems are required to operate in complex
dynamic environments and to handle functioning of highly sensitive
(security and safety-critical) organizations in government and commerce.
Typical applications include air-traffic control systems,
telecommunication networks, and banking systems. To ensure robustness,
computationally predictable behaviour and trustworthiness of these
systems, their designs and implementations must be formally well
grounded. This is an important but difficult challenge. This project
will systematically develop a framework by combining modal-logics to
adequately capture and reason about temporal, epistemic and social
aspects of dynamic and multi-agent systems. The combined logics would be
evaluated on practical applications.
An ARC funded project to run from January 2004 until December 2008.
- Design and formal verification of control and data
acquisition protocols
This research is developing new specification and verification
techniques for remote control protocols, used among interconnected sites
in supply utilities such as electricity grids, based on a proven formal
methods technology. These protocols are used in the monitoring of data
from remote sites, and the transmission of control commands to such
sites from a central location. Assurance of correctness is significant
in that incorrect protocol implementation may cause errant operation of
equipment,and lead to economic and environmental damage.
ARC Linkage Project, with Invensys Australia Ltd.
- Modelling theory for sensor networks within dynamic
landscapes
Wireless communication and device mobility are the key enabling
technologies which will determine the new computing systems to emerge
over the coming decade. These systems will have characterising features
which are quite different from traditional computing systems; features
such as mobility, dynamically changing connective topologies and direct
interaction with the landscape. These significant differences mean that
new design and analysis techniques need to be developed based on new
modelling theories, where the distinct characteristics of these emergent
systems may be readily modelled. Few existing modelling theories provide
a suitable foundation with which to model any one of the above
distinguishing characteristics; non provide an appropriate basis to deal
with all three.
We determine that a key area of research is to develop and apply new
and appropriate modelling theories to the area of pervasive, wireless
connected, mobile computing. These new systems will be complex, consist
of many interacting component devices which may move and change
connectivity through time. Rigorous and accurate models will provide us
with the means to design, analyse and understand these systems.
NICTA Fellowship.
- Design Methods for a Bushfire Sensor System
Bushfires affect the environment in a number of ways; they damage the
flora and fauna, change the landscape, and can threaten human lives.
However, the immediate effects are often hidden from observation due to
smoke and heat. New wireless sensor technology may be used in the future
to gather new data during the lifetime of the fire.
This information can be used to improve understanding of fire behavior
and to aid current fire suppression techniques.
This project will focus on modelling the use of wireless sensors to
monitor fire in bushland. The central aspects will be the effects of fire
and bush landscape on the reliability of wireless communication.
Using these results, we hope to be able to develop an accurate
model of the interaction of fire, landscape, and sensors which can
be used in a simulation environment.
The simulation environment can then be used to determine and verify the
possible ways of utilising and deploying sensors; eventually producing
guidelines for sensor applications in this domain. We use a modular
design to allow future protocols to be implemented in the simulator.
This project is Bobby Chu's PhD project, scholarship funded by
the Bushfire CRC
Recent Publicications
Conference Publications
"A heat transfer simulation model for wildfire spread". P. Johnston, G. Milne, & J.Kelso.
To appear in Forest Ecology and Management, 2006.
"Modelling Dynamically Changing Hardware Structure", G. Milne.
Proceedings of Algebraic Process Calculi 2005. In Electronic Notes in Theoretical Computer Science 162
(2006) pp. 249-254, Elsevier 2006.
"Properties as Processes: their Specification and Verification",
George Milne and Joel Kelso,
In proceedings of 25th
International Conference on Formal Techniques and Distributed Systems
(FORTE 2005). LNCS 3731, pp 503-517, Springer-Verlag, 2005
pdf (302 kb)
ppt (conference presentation) (180 kb)
Published in the
LNCS series (c) Springer-Verlag 2005.
"Building Run-time Reconfigurable Systems from Tiles",
George Milne and Gareth Lee. Proceedings of the 13th International Conference on
Field-Programmable Logic and Applications (FPL 2003), Lisbon, Portugal,
September 1-3, 2003. In Lecture Notes in Computer Science 2778,
pp. 252-261, Springer, 2003.
"A Methodology for Design of Run-Time Reconfigurable Systems",
Geroge Milne and Gareth Lee. In Proceedings of the 2002 IEEE
International Conference on Field-Programmable Technology (FPT),
Hong Kong, 16-18 December 2002. Pp. 60-67, IEEE Computer Society Press,
2002.
“A Methodology for the Formal Analysis of Asynchronous
Micropipelines”, George Milne and Antonio Cerone. Proceedings of
the Third International Conference on Formal Methods in Computer-Aided
Design (FMCAD2000), Austin, Texas, November 2000. In Lecture Notes
in Computer Science 1954, pp. 246-262,Springer, 2000.
Journal Publications
"Property verification of asynchronous systems",
Antonio Cerone and George Milne. Innovations in Systems and Software
Engineering, Vol 1, No 1, pp 25-40, April 2005, Springer-Verlag.
“Hardware Compiler Realising Concurrent Processes in
Reconfigurable Logic”, Oliver Diessel and George Milne. In IEE
Proceedings - Computers and Digital Techniques, Vol. 148, No. 4/5,
pp. 152-162, July/September 2001.
Tools
