|
|
This is a connections
and directions workshop for all
those interested in Modelling, under the
SICSA
Modelling and Abstraction research theme.
We aim to disseminate ongoing research, stimulate further
collaborations and discuss the current challenges in the field
of modelling and funding opportunities. We are also interested
in potential cross-contaminations with other research
communities.
The workshop is organised around three technical and one
EPSRC invited talks, a few
contributed short
talks, poster
presentations, a Modelling
Exercise and a discussion
section.
Invited speakers.
|= Prof. Kim G. Larsen, Aalborg University
|= Prof. David J. Pym, University of Aberdeen
|= EPSRC talk: Dr. Christina Turner, EPSRC
|= SICSA Distinguished Visitor, Prof. Alberto Policriti, Università di Udine
Participation is free but
registration is kindly requested (required for
wireless access - unless you can access eduroam
networks). Please, follow the menu on the left to access the
registration page.
|= SPEAKERS =|
Prof. Alberto Policriti |
  "Simulation by Hybrid Automata"
|
University of Udine |
We will present a technique allowing to write
programs capable to simulate Biological Networks in a
stochastic environment. We will then see how such
programs correspond, naturally, to Hybrid Automata, that
is collections of dynamical systems connected through a
discrete control network. We will conclude showing how
the Hybrid Automata resulting by the above construction
can be positioned in a lattice according to the ratio of
discreteness/continuity present in the model.
|
Prof. Kim G. Larsen |
  "Statistical Model Checking of Stochastic Hybrid Systems in UPPAAL-SMC"
|
Aalborg University |
This talk offers a survey of UPPAAL-SMC, a the major
extension of the timed automata-based verification tool
UPPAAL. UPPAAL-SMC allows for the efficient analysis of
performance properties of stochastic hybrid automata
under a natural stochastic semantics. In particular,
UPPAAL-SMC relies on a series of extensions of the
statistical model checking approach generalized to handle
real-time and hybrid systems and estimate undecidable
problems. UPPAAL-SMC comes together with a friendly user
interface that allows a user to specify complex problems
in an efficient manner as well as to get feedback in the
form of probability distributions and compare
probabilities to analyze performance aspects of
systems. The talk will detail the modeling and
specification formalisms of the tool as well as
techniques applied. Also applications to a number of
recent case studies, including Energy Aware Buildings and
Biological Systems will be presented.
|
Prof. David J. Pym |
  "Systems and Security Modelling: From Theory to Practice (Really)"
|
University of Aberdeen |
I describe a mathematical systems modelling framework
that is motivated by a desire to represent and reason about
properties of (large-scale) systems situated in dynamic environments.
Motivated by the concepts of distributed systems theory, the
framework has at its core mathematical treatments of environment,
location, resource, and process, and comes along with a separating
modal logic. Extensions to analyze questions in computer security are
also considered. The mathematical structures provide a semantics for
a modelling tool, called (Core) Gnosis, that, together with some
elementary utility theory, has been deployed in a range of commercial
projects undertaken with Hewlett-Packard's information security
business and its customers. I conclude by discussing the role of
economics in the context of modelling questions in information
security.
|
Dr. Christina Turner |
  "Modelling and the wider EPSRC context"
|
EPSRC |
Further information about the Theme's main page can
be
found here. The related team contact page
is here.
|
|= PROGRAMME =|
11th June 2012
Cottrell Building
University of Stirling
Time
| Room
| |
|
9:00-09:50 |
2A9 |
|
Welcome, Poster Session and Coffee |
9:50-10:20 |
W1 |
|
SICSA Distinguished Visitor: Alberto Policriti |
|
|
|
"Simulation by Hybrid Automata" |
10:20-11:20 |
W1 |
|
Short talks
Gregory Goltsov "3D agent-based thrombus formation multi-scale model with Hybrid Functional Petri nets signalling network modelling"
Carron Shankland "Optimisation of Process Algebra Models Using Evolutionary Computing"
Marwan Fayed "Network Description: Increasingly Elusive Features"
Bruce Graham "Modelling and the Brain"
|
11:20-12:20 |
W1 |
|
Invited talk: Kim G. Larsen |
|
|
|
"Statistical Model Checking of Stochastic Hybrid Systems in UPPAAL-SMC" |
12:20-13:45 |
2A9 |
|
Poster Lunch |
13:45-14:30 |
W1 |
|
Modelling Exercise Selected Presentations (3x) |
14:30-15:30 |
W1 |
|
Invited talk: David J. Pym |
|
|
|
"Systems and Security Modelling: From Theory to Practice (Really)" |
15:30-16:15 |
W1 |
|
EPSRC talk: Christina Turner (teleconference) |
|
|
|
"Modelling and the wider EPSRC context" |
16:15-16:45 |
2A9 |
|
Modelling Exercise Coffee Break |
16:45-18:00 |
W1 |
|
Final Discussion and Closing |
|= MODELLING EXERCISE =|
The Modelling Exercise consists of the development of a
suitable model of a proposed system and the use of the model to
better understand the system. Reasoning about and
understanding (the model of) the system may involve both
simulation and analysis/reasoning, as well as any other
preferred approach.
The Modelling Exercise will be carried out by teams, free
to use their preferred tools and modelling
approach. Teams must develop a model of
one of the systems proposed below and use it to gain knowledge
about the system along the suggested lines. Initial
reference are provided, but they can clearly be expanded, if
suitable. Results of the exercise, i.e. models and related
analyses, will be evaluated in terms of
accuracy of the model,
relevance of the analysis
results, suitability/efficiency of
the approached proposed and
heterogeneity of the team. Teams will preferably be
formed across different existing research groups.
The Modelling Exercise organisers will select the best
three results that will be summarised at the workshop and voted
by the audience.
Schedule
5th May |
Modelling Exercise call. Suggestions about the system to be modelled are welcome. |
24st May |
System to be modelled is published. Team registration opens. |
6th June |
Deadline for
submitting results. |
Please, submit a brief report of your
results by e-mail to Andrea Bracciali. Please keep your report
simple and informal (5 pages at most, say). You may provide references to a web
page, if you wish.
11th June |
Workshop: presentation of selected results and prizes. |
Modelling Problems
|= Circadian clock |
Overview
This is a biological system in which a clock or oscillatory
behaviour emerges by the interaction of its components, supposedly regulated by
a few molecules and their passage of
states.
|
|
Abstract
Circadian rhythms are very important mechanisms which
regulate many processes in many organisms. It is
believed they are driven via transcription in higher
organisms or via phosphorylation (ie., informally, an activation mechanism) in lower organisms.
We are interested in a model of a clock present in Cyanobacteria, which involves the rhythmic phosphorylation of
the protein KaiC. The KaiC
protein forms complexes of six KaiC joined together (a hexamer).
Therefore a single KaiC hexamer can exist in 7 stages of phosphorylation
with 0 to all 6 of its single KaiC proteins phosphorylated.
The clock has been shown to persist in vitro in the presence of only KaiA,
KaiB, KaiC and ATP. KaiA and KaiB form dimers and are known to form
complexes with KaiC hexamers although such polymers do not contain more
than a single KaiC hexamer. So we know that a single KaiC hexamer cycles
through these states of varying degrees of phosphorylation. The question is
can you produce a model in which
there is an oscillating concentration/population of
phosphorylated KaiC hexamers (expectedly regulated by KaiA and KaiB)? In addition does your
model still allow this when there is a non-saturated
population of unbound KaiA protein, that is the
concentration/population of unbound KaiA dimers is not
close to zero?. KaiA appears to stimulate
phosphorylation whilst KaiB appears to interfere with
this effect.
One possibility is that the KaiC monomers may be in either an active or
inactive state, whereby the active state promotes phosphorylation and the
inactive state promotes dephosporylation. It is thought that the energetic cost of a
single KaiC hexamer containing two monomers in different active-inactive
configurations is prohibitively high and therefore the entire KaiC hexamer
is either in the active or the inactive state. Therefore a single KaiC
hexamer can exist in 14 states corresponding to the 7 degrees of
phosphorylation in both the active and inactive states. More information
and a model of this explanation can be found in van Zon et 2007[1].
|
|
References
[1] van Zon,
Lubensky, Altena, ten Wolde. An allosteric model of
circadian KaiC phosphorylation. PNAS 104(18) (2007)
7420-7425
See also [2]Hakuto Kageyama, Takao Kondo and Hideo
Iwasaki. Circadian
Formation of Clock Protein Complexes by KaiA, KaiB,
KaiC, and SasA in Cyanobacteria
|
|= Emergency egress |
Overview This is an example
of crowd dynamics, where a multitude of individuals
(agents/components) interact within a physical
environment. How do they "collectively" escape from a
building? What more elaborated behaviour of the singles and of the crowd can be described and analysed?
|
|
Abstract The analysis of
crowd dynamics shows emergent patterns of behaviour,
which result from the interaction of the many
individuals comprising a crowd. In this case the
behaviour of a crowd evacuating a prototype building
has to be modelled. The initial conditions of the
system are described
in
Appendix C of [1]. This is the user manual of
EVACNET4, a tool for the modelling of building egress
based on a capacitated network flow transhipment
algorithm and used for the generation of optimal
building evacuation plans. The case study description
includes details of human factors such as how fast people
cover a certain distance on average and how many
people may pass on average through a standard door in
a given time period. The mentioned appendix contains
a detail description of a three storey building and
assumptions about "standard" human behaviour that can
be expected in the described situation.
Being based on an optimisation approach, the tool
does not appear flexible enough to model the many
"non-optimal" evacuation patterns and different human
behaviours that can occur during an evacuation. The
question is how can we devise a
model of the dynamics of the building egress that is
"safe", as it properly models aspects such as egress
times and room occupancy, and "expressive", as it
allow individual behaviours and non-standard
situations - the one that more often recur in
emergencies - to be easily embedded in the model and
analysis?
You should use the results in [1] as a sanity check
for your model. You may take inspiration from [2], about
examples of behaviours and situations you may wish to
embed in your model for making it more realistic and use
it for interesting analysis exploiting your preferred
techniques.
|
|
References
[1] T. M. Kisko, R. L. Francis and
C. R. Nobel. EVACNET4
USER'S GUIDE University of Florida
[2]
Gabriel Santos and Benigno
Aguirre.
A critical review of Emergency evacuation simulation
models NIST ws on Building Occupant Movement during Fire Emergency.
|
|= Software Patching Optimisation |
Overview This example
concerns the use of software patching to overcome
emerging security flaws in computer networks. The
deployment of patches is expensive - causing
disruption to service, but essential to avoid exposure
to security attacks.
|
|
Abstract In recent years the
economics of information security has been an important
topic of research (for a survey see [1], and for a
cost-benefit analysis see [2]). In [3] a mathematical
model is presented based on the confidentiality and
availability trade-off involved in patching. This model
uses a method called linear stabilization. Specifically
a decision maker minimises a loss function, defined in
terms of the confidentiality C(t), Availability A(t) and
investment K(t). A solution is defined as a definite
integral. Patches are interpreted as shocks to C(t) and
A(t) and are assumed to have Poisson-type arrival times
and bivariate log-normal intensities. Numerical
simulations are generated for different parameter
choices. In particular, the paper considers the
difference in patching profiles observed for military
and financial software systems.
The model could be extended in various directions. For
instance, others approaches than numerical simulations could be
introduced and strong assumptions (e.g. in the
distribution of arrival times) relaxed. Flexibility in the sense of allowing
for alternative assumptions could be sought as well.
The question is how can we devise a model of the system that clarifies the system under investigation and either:
- Allows for verification, or, at the very least allows for more extensive simulation
- Allows for a less restrictive (or at least an alternative) set of assumptions?
You should use the model in [3] to inform your model.
|
|
References
[1] R. Anderson and T. Moore. The economics of information Security. Science, 314:610-613, 2006.
[2] L. Gordon and M. Loeb. Managing Cybersecurity Resources: A cost-benefit Analysis. McGraw Hill, 2006.
[3] Christos Ioannidis, David Pym, and Julian Williams.Information Security Trade-offs and Optimal Patching Policies.
European Journal of Operational Research, 216(2):434-444, 16 January 2012. doi:10.1016/j.ejor.2011.05.050.
Pre-print available at http://www.abdn.ac.uk/~csc335/IoannidisPymWilliams-EconPatching.pdf
|
Organisers
Andrea Bracciali
|
University of Stirling
|
Allan Clark
|
University of Edinburgh
|
Alice Miller
|
University of Glasgow
|
Gethin Norman
|
University of Glasgow
|
|= CONTRIBUTIONS =|
Contributions
about ongoing and
mature results, as well overviews of
groups' research are sought. All the proposed contributions
are expected to be presented in the form of
a poster (up to space
availability and relevance for the workshop). Selected contributions will be invited for
a short oral
presentation. PhD students are
particularly encouraged to submit contributions. A number of
slots is reserved for their contributions.
A book of abstracts will be published
as a Technical Report by Computing Sciences and Mathematics at
the University of Stirling.
For each contribution, a short
abstract should be submitted
to Andrea Bracciali
preferably by 1st of June. Please, just
send a text file by e-mail with subject "MCP2012
contribution".
|= REGISTRATION =|
The workshop is sponsored by SICSA
and Computing Science and
Mathematics at the University of Stirling.
Participation is free and welcomed, registration is kindly requested (required for wireless access - see below). There are two types of registrations:
- Participants register here.
- Teams for the Modelling Exercise register here. A team name has to be decided and created by the first member registering.
Wireless access will be provided to all the registered participants. Please provide a few days for dealing with your registration. An Eduroam Network is being installed, too.
|= LOCATION =|
The workshop will be held in room
2W1 on the ground floor (2) in
corridor W of
the Cottrell Building at the
University of Stirling. See
a map of the building for directions (You
will probably be arriving in Queen's Court).
The campus of the University
of Stirling is just outside the city of Stirling.
Detailed information about how to reach the campus can be
found here.
If you are traveling by public
transport, perhaps the best option is to reach Stirling
by train, and then get either a bus (1.20 GBP) or a taxi
(about 5-7GBP) to the campus.
If you are traveling by car, follow
the driving directions in the web page above and be aware that
you need to report to the gate as a visitor attending the
workshop: you will receive a parking permit. If possible, park
in the parking lot next to the Cottrell Building, opposite
Queen's Court.
|
|