Research Proposal - Live formal models for predictable pervasive systems - Muffy Calder
Pervasive computing systems are characterised by the integration of computation into everyday objects, devices and activities. They are often component-based systems dependent on their virtual or physical environment. Two examples are a sensor-based home care system and a mobile, multiple player phone-based game; both consist of several components, each of which may be off the shelf (e.g. a motion detector) or a modification of existing components (e.g. make your own android phone application). Components and environments change: you download a new app or change a setting on one, you move from within a broadband network to a telephone network, a component is stationary or moving (e.g. on a train), the ambient temperature is above or below freezing. Behaviours and resource usages change accordingly, e.g. a component delivers data to another component every 10 minutes if it is stationary and every 5 seconds if is moving, or it consumes more power and money if it is connected through a telephone network rather than through wifi.
My research aims to predict the effect of change, e.g. if we add, remove or update a component, or move one component or the whole system to another physical space, or change the rate of some events, or change the operating environment, does the system still work, and how much resource (e.g. power and money) will it consume? For example, will I have enough power left to receive a crucial call at 17:00 and will I stay within a monthly agreed expenditure?
I will answer these questions by developing new, formal computational models of components, environments, and what it means to work and consume resource. The models are live: extracted from the components while the system is running, so that the system or user can predict behaviour before committing to a change. The answers may be a probability distribution, rather than simply yes or no, e.g. it is 85% likely there will be enough power left at 17:00 if you download this new app, or 90% likely there will be no false alarms from this home care system.
The long term impact is pervasive systems that work and consume predictable resource: truly plug and play software systems we can trust and use, wherever and whenever.
Summary: I will develop practical, formal models and reasoning techniques to make context-dependent, component-based software systems more predictable and usable. I will build on my recent work on pervasive interface automata for interfaces, linear temporal logics for services, and model-checking techniques for automated reasoning. A novelty is the way models are used: online, to feed back results to the system. This is a radical departure from the traditional use of formal methods.
Background: A model has the form: C1 x C2 x … Cn where each Ci is a pervasive interface (PI) automaton for a component interface. The x (composition) operator denotes components are composed (i.e. running concurrently), and synchronise on calling/callable methods. A system can be considered in an environment, which is also a composition. A system works in an environment when it offers a desired service, which is expressed in a temporal logic. The critical relation is C1 x C2 x …x Cn |= S, where S is a formula for the service in a logic and |= denotes satisfaction of that formula. Predictability depends on the key questions, assuming C and E are compositions of PI automata: i) under what conditions does C x E |= S (does the system work in an environment) and how are the conditions specified, ii) when C x E |= S, under what conditions can we replace C by C1 and have C1 x E |= S (does the system still work if we replace C by C1) and how are the conditions specified, and iii) when does an environment meet a set of conditions.Conditions are specified by two sets of (state, action) pairs, denoting actions the environment must and must not offer, for given system states.The trick is not to compute the |= relation, which would involve actually making the composition or change, but to define a relation |=A over a more abstract model constructed from A, and to compute this relation by model checking.
Aims: Extend the basic theory in several ways, to make it more expressive, more applicable, and more automated. This includes: adding continuous time resource consumption and events, topological and metric space, probabilistic and non-probabilistic events, and broadcast communication; extensions to replacement taking into account resource, physical location and behaviour likelihoods; techniques to model-check reasoning requirements for replacement; extraction of the automata automatically from code and annotations; and validation all of the above in several case studies.