Modern society faces a fundamental problem: the reliability of complex, evolving software systems on which it critically depends cannot be guaranteed by the established, non-mathematical techniques, such as informal prose specification and ad-hoc testing. Modern companies are moving fast, leaving little time for code analysis and testing; concurrent and distributed programs cannot be adequately assessed via traditional testing methods; users of mobile applications neglect to apply software fixes; and malicious users increasingly exploit programming errors, causing major security disruptions. Trustworthy, reliable software is becoming harder to achieve, whilst new business and cyber-security challenges make it of escalating importance. Developers cope with complexity using abstraction: the breaking up of systems into components and layers connected via software interfaces. These interfaces are described using specifications: for example, documentation in English; test suites with varying degrees of rigour; static typing embedded in programming languages; and formal specifications written in various logics. In computer science, despite widespread agreement on the importance of abstraction, specifications are often seen as an afterthought and a hindrance to software development, and are rarely justified. Formal specification as part of the industrial software design process is in its infancy. My over-arching research vision is to bring scientific, mathematical method to the specification and verification of modern software systems. A fundamental unifying theme of my current work is my unique emphasis on what it means for a formal specification to be appropriate for the task in hand, properly evaluated and useful for real-world applications. Specifications should be validated, with proper evidence that they describe what they should. This validation can come in many forms, from formal verification through systematic testing to precise argumentation that a formal specification accurately captures an English standard. Specifications should be useful, identifying compositional building blocks that are intuitive and helpful to clients both now and in future. Specifications should be just right, providing a clear logical boundary between implementations and client programs. VeTSpec has four related objectives, exploring different strengths of program specification, real-world program library specification and mechanised language specification, in each case determining what it means for the specification to be appropriate, properly evaluated and useful for real-world applications. Objective A: Tractable reasoning about concurrency and distribution is a long-standing, difficult problem. I will develop the fundamental theory for the verified specification of concurrent programs and distributed systems, focussing on safety properties for programs based on primitive atomic commands, safety properties for programs based on more complex atomic transactions used in software transactional memory and distributed databases, and progress properties. Objective B: JavaScript is the most widespread dynamic language, used by 94.8% of websites. Its dynamic nature and complex semantics make it a difficult target for verified specification. I will develop logic-based analysis tools for the specification, verification and testing of JavaScript programs, intertwining theoretical results with properly engineered tool development. Objective C: The mechanised specification of real-world programming languages is well-established. Such specifications are difficult to maintain and their use is not fully explored. I will provide a maintainable mechanised specification of Javascript, together with systematic test generation from this specification. Objective D: I will explore fundamental, conceptual questions associated with the ambitious VeTSpec goal to bring scientific, mathematical method to the specification of modern software systems.

The ecosystem of compute devices is highly connected, and likely to become even more so as the internet-of-things concept is realized. There is a single underlying global protocol for communication which enables all connected devices to interact, i.e. internet protocol (IP). In this project, we will create a corresponding single underlying global protocol for computation. This will enable wireless sensors, smartphones, laptops, servers and cloud data centres to co-operate on what is conceptually a single task, i.e. an AnyScale app. A user might run an AnyScale app on her smartphone, then when the battery is running low, or wireless connectivity becomes available, the app may shift its computation to a cloud server automatically. This kind of runtime decision making and taking is made possible by the AnyScale framework, which uses a cost/benefit model and machine learning techniques to drive its behaviour. When the app is running on the phone, it cannot do very complex calculations or use too much memory. However in a powerful server, the computations can be much larger and complicated. The AnyScale app will behave in an appropriate way based on where it is running. In this project, we will create the tools, techniques and technology to enable software developers to create and deploy AnyScale apps. Our first case study will be to design a movement controller app, that allows a biped robot with realistic humanoid limbs to 'walk' over various kinds of terrain. This is a complex computational task - generally beyond the power of embedded chips inside robotic limbs. Our AnyScale controller will offload computation to computers on-board the robot, or wirelessly to nearby servers or cloud-based systems. This is an ideal scenario for robotic exploration, e.g. of nuclear disaster sites.

Users want mobile devices that appear fast and responsive, but at the same time have long lasting batteries and do not overheat. Achieving both of these at once is difficult. The workloads employed to evaluate mobile optimisations are rarely representative of real mobile applications and are oblivious to user perception, focussing only on performance. As a result hardware and software designers' decisions do not respect the user's Quality of Experience (QoE). The device either runs faster than necessary for optimal QoE, wasting energy, or the device runs too slowly, spoiling QoE. SUMMER will develop the first framework to record, replay, and analyse mobile workloads that represent and measure real user experience. Our work will expose for the first time the real Pareto trade-off between the user's QoE and energy consumption. The results of this project will permit others, from computer architects up to library developers, to make their design decisions with QoE as their optimisation target. To show the power of this new approach, we will design the first energy efficient operating system scheduler for heterogeneous mobile processors which takes QoE into account. With heterogeneous mobile processors just now entering the market, a scheduler able to use them optimally is urgently needed. We expect our scheduler to be at least 50% more energy efficient on average than the standard Linux scheduler on an ARM BIG.LITTLE system.