 |
| |
Current projects
-
Extending the Scope of Modular Analysis for the Validation of Large Systems
Funding: ARC Linkage Grant 2004, France-Australia Science and Technology grant 2004-2006
Participants: Laure Petrucci, Jonathan Billington, Christine Choppy, Charles Lakos
The increasing complexity of computer systems has severe
implications for verification and validation, which is especially
important for critical systems (e.g., medical supervision,
avionics mission systems). The standard approach is to build a
formal model of the system and then attempt to analyse it. The
use of state space techniques is an important method
facilitating automatic analysis. However, the number of states
is usually so large as to preclude analysis. The modular
analysis technique proposed in this project reduces the state
space by matching the analysis technique to the structure of
the model. Preliminary results are promising and motivate the
extension of the technique to a larger class of modular
descriptions.
The project will extend the applicability of modular analysis,
so as to support coupling of modules via resource sharing. The
derivation of optimisation strategies for the placement of
resources will lead to a significant performance gain. Handling
timed systems is also a theoretical and practical challenge. A
third extension is the identification of data independence at the
interface between modules resulting in a significant increase in
size and complexity of the systems that can be analysed. These
extensions will be implemented in the Design/CPN tool, where
they can be used for the evaluation of several non trivial case
studies.
Funding: ARC Discovery Grant, 2004-2006
Participants
David Hemer, University of Adelaide
Colin Fidge, Queensland University of Technology
Phil Cook, University of Queensland
Processor obsolescence is a serious maintenance problem
for long-lived computer control systems in military aircraft and other
critical applications. A promising solution is to interpose an emulator
program between the old "legacy" software and a replacement processor.
Unfortunately, no
techniques exist for proving that this procedure preserves the original
system's functional and timing behaviour. A particular challenge is
that processor emulations involve both legacy code and new subroutines,
written in different programming languages. Furthermore, the new system
is unlikely to exactly duplicate the timing of the original one, so it
must be possible to recognise acceptable differences. This project will
show how rigorous "change impact analyses" can be applied to emulated
software, to accurately determine the extent of changes introduced by
an emulator-based software upgrade.
-
Plug-in proof support for formal development
environments
Funding: University of Adelaide Small Research Grant, 2005
Participants: David Hemer
For critical applications, mathematical-based techniques
are often employed to increase confidence in the software. Formal
development environments (FDEs) help apply these techniques. However
when it comes to proving properties, as is required for critical
software, FDEs are not as powerful as standalone prover tools. We aim
to connect standalone provers to FDEs using a framework that translates
FDE properties into a form that is readable by the provers. In order to
ensure that the translation is mathematically sound, this project will
develop an approach to translating properties to theorem provers in a
systematic manner, rather than the current ad-hoc approaches.
-
The Analysis of Timed Systems using Relative Time Petri Nets
Participants: Joseph Kuehn, Charles Lakos, Rob Esser
-
The Development of Embedded Systems
Participants: David Knight, Charles Lakos, David Hemer, Rob Esser
-
High-Level Synthesis of Asynchronous Systems
Participants: Sue Tyerman, Charles Lakos, David Hemer
-
Participants: Charles Lakos
Object Petri Nets (OPNs) extend the formalism of
Coloured Petri Nets with a complete integration of object-oriented
features, including inheritance, polymorphism and dynamic binding. The
object-orientation provides powerful structuring primitives allowing
the modelling of complex systems, including those with multiple levels
of activity.
Proposed projects
-
The Analysis of Mobile Systems using Mobile Petri Nets
Participants: Charles Lakos
Mobile systems explore the interplay between locality
and connectivity. A subsystem may have a connection to a
remote subsystem and use this for communication. Alternatively,
it may be necessary or desirable to move the subsystem close
to the other in order to communicate. A Petri Net
formalisation has been proposed for mobile systems so as to
harness the intuitive graphical representation of Petri Nets
and the long history of associated analysis techniques.
This project will explore techniques suitable for the analysis
of mobile systems defined in this formalism for Mobile Petri Nets.
For example, a model for IETF Mobile IP protocol has been defined
and is currently being analysed.
-
The Analysis of Network Protocols by means of Protocol Subsets
Participants: Charles Lakos
Business and social infrastructure worldwide is becoming
increasingly dependent on the Internet and the protocols it uses.
(A protocol specifies the rules for the orderly exchange of data).
The use of flawed protocols to transfer information is clearly
undesirable, but their complexity presents difficulties for
automated verification techniques. One common engineering approach
is to verify protocol subsets, for example, by limiting the number
of communicating parties or the capabilities provided.
This project will formalise this approach and determine when such
partial verifications can be extrapolated to the complete
protocol. It is therefore anticipated that this research will
create new knowledge and techniques for verifying complex network
communication protocols.
-
The Application of Modern Heuristic Techniques to the
Verification of Complex Concurrent Systems
Participants: Charles Lakos, Zbigniew Michalewicz
The ever-increasing complexity of software systems outstrips our
ability to verify their correctness. Traditional techniques are
fundamentally limited: testing examines system response to
selected scenarios and cannot guarantee the absence of errors;
model checking, by contrast, explores all possible system states -
and can guarantee correctness but only if the number of states is
manageable, which is not the case for complex systems.
Heuristic techniques have been applied to complex optimisation
problems, where they complement exact and complete algorithms,
and have proved effective in finding good, approximate solutions.
This project will explore whether similar benefits can be
achieved by adapting heuristic algorithms to verification.
-
The Relationship between Modular Analysis and Partial Order Reduction
Participants: Charles Lakos
The modular analysis of concurrent systems takes advantage
of the modular structure of such systems. It treats the local
activity of each module as essentially independent of the local
activity of other modules. This avoids exploring every possible
interleaving of the local activity of the various modules, which
can be a significant contributor to the problem of state space
explosion.
Partial order reduction attempts to avoid the state space
explosion problem due to arbitrary interleavings by defining a
global view of independent activities. At each state, only a set
of dependent activities are explored.
This project will explore the relationship between these two
notions of independent activities. The goal will be to formalise
the relationship and develop efficient algorithms for the analysis
of modular concurrent systems.
Previous projects
-
A Category Theoretic Approach to Inconsistencies in Modular System Specification
Participants: Catherine Menon, Mike Johnson, Charles Lakos, Sylvan Elhay
Inconsistency management is fundamental to effective system
specification. This thesis presents a categorical approach to
the detection, classification and resolution of those
inconsistencies which commonly arise in modular systems.
This categorical approach relies upon the generation of the
Categorical Consistency Framework, within which inconsistencies
can be represented separately from implementation details.
Using this framework, we construct a taxonomy of inconsistencies,
presenting metrics for determining their severity and discussing
a number of resolution methods. We also show how this framework
can be used to combine multiple specifications into a single
consistent system and predict the behaviour of this system. In
the process, we adapt existing work relating to the database
view update problem to system specification. This enables us
to analyse the probable underlying system behaviour, given the
behaviour of individual components. We also introduce the
notion of degrees of consistency, a concept which allows us
to examine how well a system recovers from system failure.
-
Compositional Verification of Component-Based Heterogeneous Systems
Participants: Yan Jin, Rob Esser, Charles Lakos
Mathematically-based formal specification and verification
methods can provide substantial help in revealing ambiguity and
inconsistency of informal system descriptions, and increase
confidence in the correctness of system designs. However, as
their complexity rapidly grows, modern computer-based systems
often consist of parts (or subsystems) with very different
characteristics, e.g. data-centred vs. control-oriented.
Traditional formal methods relying on a single specification
language are no longer appropriate for coping with all aspects
of such a system. A combination of languages to be used for
system specification is required.
This thesis focuses on discrete-event systems and a class of
specification languages, viz. graph-like visual languages. It
takes a two-step approach to study these fundamental issues and
seek practical, tool-supported solutions. Firstly, an underlying
methodological framework is proposed, which is built on a solid
semantic base of interconnected discrete-event components.
Secondly, this thesis focuses on model checking, a robust and
largely automatic approach to system formal verification. It
proposes a compositional approach to combat the state space
explosion problem, a well-known obstacle to model checking.
This compositional approach is implemented as automated tools in
the context of the Moses tool suite. These tools are then applied
to the verification of a non-trivial distributed embedded system
Ñ the Production Cell. It is shown that a significant reduction
in complexity of system verification is achieved.
-
Participants: Rob Esser, Yan Jin, Joseph Kuehn
The Moses project focuses on the modelling, simulation,
implementation, and evaluation/verification of heterogeneous systems.
Systems are typically described using modeller friendly, visual
languages. Moses supports the definition of the syntax and semantics of
these languages in an integrated environment. Recent work includes the
verification of component based data-flow process networks.
-
Participants: Peter Ashenden, Rob Esser, Catherine Menon, Kylie Williams, Joseph Kuehn
Rosetta is a language that allows the specification of
functional requirements and constraints in multiple interacting domains
at varying levels of abstraction. Rosetta has a formal semantic basis,
but also provides modelling support for different design domains,
employing specific semantics and syntax appropriate for each. Each of
these domains provides a semantic and representational framework for
presenting information particular to that domain. In addition, interactions
are defined between these domains to allow for information stored in
models in different domains to influence each other to enable overall
design of a system specification.
|
|
