Science of Sensor Systems Software

Towards a unifying science for smarter sensor based systems

We will deliver new principles and techniques for the development and deployment of verifiable, reliable, autonomous sensor systems that operate in uncertain, multiple and multi-scale environments.

About

Science of Sensor Systems Software (S4) is an EPSRC programme grant for Glasgow University with Universities of St Andrews, Liverpool and Imperial College running from January 2016 until December 2020.

View more »

Investigators

Prof. Muffy Calder (overall PI, Glasgow)
Prof. Simon Dobson (St Andrews)
Prof. Michael Fisher (Liverpool)
Prof. Julie McCann (Imperial College)

View more »

Partners

S4 will be driven and validated by end-user and experimental applications involving ten organisations, including ABB, British Geological Survey, CENSIS, Freescale, Rolls-Royce, Thales, and Transport Scotland.

View more »

Research vision

Sensor systems are embedded everywhere: from transportation and lighting, to smart tags and flooded fields, providing information and facilitating real-time decision-making and actuation. Smart cities, internet of things, big data and autonomous vehicles all depend on robust sensor systems that can be trusted to deliver useful, timely and more reliable information.

Extracting information is far from straightforward: sensors are noisy, they decalibrate or may be misplaced, moved, compromised, and generally degraded over time, both individually and as a collective network. Uncertainty pervades the physical and digital environments in which the systems operate. There are increasing requirements to add more autonomy and intelligence, yet we understand very little about programming in the face of such pervasive uncertainty that cannot be engineered away. How can we be assured that a sensor system does what we intend, in a range of dynamic environments? How can we make such a system “smarter”? How can we connect the stochastic nature of environments, the continuous nature of physical systems, and discrete nature of software? Currently we cannot answer these questions because we are missing a science of sensor system software. The S4 programme will develop a unifying science, across the breadth of mathematics, computer science and engineering, that will let developers engineer for the uncertainty and ensure that their systems and the information they provide is resilient, responsive, reliable, statistically sound and robust. The vision is smarter sensor based systems in which scientists and policy makers can ask deeper questions and be confident in obtaining reliable answers, so the programme will deliver new principles and techniques for the development and deployment of verifiable, reliable, autonomous sensor systems that operate in uncertain, multiple and multi-scale environments.

Diagram



The dashed arrows indicate the elements to be developed: linking software development and sensor system applications, deployment and the frames of reference that determine the dimensions of environment in which the systems operate.

News


7 December 2016 Prof Julie McCann delivered a distinguished seminar at the School of Computing & Communications, Lancaster University. The title of the talk was Are Sensor Networks a first step towards the Diamond Age?

7 November 2016 Prof Julie McCann delivered a set of distinguished lectures centred around Distributed Systems and Sensing at the School of Computer Science, University of St Andrews.

14 October 2016 Second all-hands meeting located at Imperial College London. Take a look at our group photo!

13 October 2016 Interest meeting on the Gossip and the Firefly protocols at Imperial College London.

15 June 2016 Dr Sven Linker will join us as postdoctoral researcher in Liverpool, starting on 1 August 2016. He is currently a Research Fellow in the School of Computing, Engineering and Mathermatics, University of Brighton.

25 - 26 April 2016 The first all-hands meeting was a resounding success: interesting talks generating many discussions around them, activities and research goals planned for the following months. Take a look at our dinner photo!

10 March 2016 The press release in the Imperial College London news about S4 as a new project that will ensure information gathered by sensors is reliable.

11 February 2016 We are seeking two Postdoctoral Research Associates in Formal Verification of Autonomous Sensor Network Software at University of Liverpool. More details can be found here.

1 February 2016 Our kick off meeting will take place in Glasgow on 25 - 25 April 2016.

29 January 2016 More digital press articles about us: Herald Scotland, Osborne Clarke, Global Post, Daily Record, CENSIS, my Science, v3, Machinery Market, Internet of Business.

11 January 2016 First press releases in the University of Glasgow news, University of Liverpool news.

5 January 2016 The S4 programme started! Let's roll!

People


Muffy Calder

Prof Muffy Calder

Overall PI

View profile »

Michael Fisher

Prof Michael Fisher

Investigator

View profile »

Simon Dobson

Prof Simon Dobson

Investigator

View profile »

Julie McCann

Prof Julie McCann

Investigator

View profile »

Alice Miller

Dr Alice Miller

Senior Lecturer

View profile »

Clare Dixon

Dr Clare Dixon

Senior Lecturer

View profile »

Oana Andrei

Dr Oana Andrei

Research Fellow

View profile »

Michele Sevegnani

Dr Michele Sevegnani

Research Fellow

View profile »

Lei Fang

Dr Lei Fang

Research Fellow

View profile »

Sven Linker

Dr Sven Linker

Research Fellow

View profile »

Michael Breza

Dr Michael Breza

Research Associate

View profile »

Matt Webster

Dr Matt Webster

Research Associate

View profile »

Lynne Brown

Ms Lynne McCorriston

Business Development Manager

View profile »

Projects


Foundations

Objectives: To develop the new foundational conceptual frameworks, theories, models, logics and reasoning techniques needed for analysis of capabilities, constraints and requirements of sensor system software.
Leader: Prof Muffy Calder with expertise in stochastic event-based modelling and reasoning, multi-scale and spatial modelling for virtual/physical systems, decision support for event-based condition monitoring, real-time verification, component-based modelling for biochemical systems and probabilistic analysis of software usage.

Verification

Objectives: To develop new techniques and tools for the abstract design and formal verification of both individual and ensemble behaviours of autonomous sensor systems.
Leader: Prof Michael Fisher with expertise in practical formal methods, temporal logics, programming languages, and the formal verification of autonomous systems.

Adaptation

Objectives: To develop the approaches that match the formal understanding of the problem space and the mission of a sensor network to its realisation, deployment, and adaptation in the field.
Leader: Prof Simon Dobson with expertise in building adaptive sensor technology to observe complex real-world processes in ways that respect end-to-end scientific constraints.

Engineering

Objectives: To build a framework that enhances the programmability and maintainability of next-generation sensor/actuator systems at scale and that can also take as dynamical inputs control functionality and verification probes while supplying the data representing the frames of reference as assessed by the framework at run-time as measures of dynamic environmental context.
Leader: Prof Julie McCann with expertise in decentralised algorithms and protocols for low-powered sensing and control systems that dynamically adapt to their environments.

Partners

S4 will be driven and validated by end-user and experimental applications involving the following organisations: ABB, British Geological Survey, CENSIS, Freescale, Jacobs, Rolls-Royce, Scottish Canals, Thales, Topolytics, Transport Scotland.

Publications

2017

Muffy Calder and Michele Sevegnani. Stochastic model checking for predicting component failures and service availability. IEEE Transactions on Dependable and Secure Computing, 2017.

2016

Louise A. Dennis, Marija Slavkovik, and Michael Fisher. ”How Did They Know?” - Model-Checking for the Analysis of Information Leakage in Social Networks. In Proc. of Joint Workshop on Coordination, Organizations, Institutions and Norms and Norms in Multiagent Systems, 2016. To appear in Springer LNCS.

Michele Sevegnani and Muffy Calder. BigraphER: Rewriting and Analysis Engine for Bigraphs. In S. Chaudhuri and A. Farzan, editors, Proc. of 28th International Conference on Computer Aided Verification (CAV’16), volume 9780 of Lecture Notes in Computer Science, pages 494–501. Springer, 2016.

Steve Benford, Muffy Calder, Tom Rodden, and Michele Sevegnani. On Lions, Impala, and Bigraphs: Modelling Interactions in Physical/Virtual Spaces. ACM Trans. Comput. Hum. Interact., 23(2):9:1–9:56, 2016.

Oana Andrei, Muffy Calder, Matthew Chalmers, Alistair Morrison, and Mattias Rost. Probabilistic Formal Analysis of App Usage to Inform Redesign. In E. Abraham and M/ Huisman, editors, Proc. of the 12th International Conference on Integrated Formal Methods (iFM’16), volume 9681 of Lecture Notes in Computer Science, pages 115–129. Springer, 2016.

Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman, and Sandor Veres. Autonomous Agent Behaviour Modelled in PRISM: A Case Study. In D. Bosnacki and A. Wijs, editors, Proc. of the 23rd International SPIN Symposium on Model Checking of Software (SPIN’16), volume 9641 of Lecture Notes in Computer Science, pages 104–110. Springer, 2016.

2015

Marija Slavkovik, Louise A. Dennis, and Michael Fisher. An abstract formal basis for digital crowds. Distributed and Parallel Databases, 33(1):3–31, 2015.

Muffy Calder, Philip D. Gray, and Chris Unsworth. Is my configuration any good: checking usability in an interactive sensor-based activity monitor. ISSE, 11(2):131– 142, 2015.

Po-Yu Chen, Shusen Yang, and Julie A. McCann. Distributed Real-Time Anomaly Detection in Networked Industrial Sensing Systems. IEEE Transactions on Industrial Electronics, 62(6):3832–3842, 2015.

Lei Fang and Simon Dobson. Towards data-centric control of sensor networks through Bayesian dynamic linear modelling. In Proc. of the Ninth IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO’15), 2015.

Sokratis Kartakis, Edo Abraham, and Julie A. McCann. WaterBox: A Testbed for Monitoring and Controlling Smart Water Networks. In Proc. of the 1st ACM International Workshop on Cyber-Physical Systems for Smart Water Networks (CySWater’15), 2015.

Savas Konur and Michael Fisher. A roadmap to pervasive systems verification. Knowledge Eng. Review, 30(3):324–341, 2015.

Pedro M. N. Martins and Julie A. McCann. The Programmable City. In Elhadi M. Shakshuki, editor, Proc. of the 6th International Conference on Ambient Systems, Networks and Technologies (ANT 2015), volume 52 of Procedia Computer Science, pages 334–341. Elsevier, 2015.

Michele Sevegnani and Muffy Calder. Bigraphs with sharing. Theoretical Computer Science, 577:43–73, 2015.

Saray Shai, Dror Kenett, Yoed Kenett, Miriam Faust, Simon Dobson, and Shlomo Havlin. Critical tipping point distinguising two types of transitions in modular network structures. Physical Review E, 2015.

Emanuele Strano, Saray Shai, Simon Dobson, and Marc Barthélemy. Multiplex networks in metropolitan areas: generic features and local effects. Journal of the Royal Society Interface, 12(111), 2015.

Juan Ye, Graeme Stevenson, and Simon Dobson. Fault detection for binary sensors in smart home environments. In Proc. of the IEEE International Conference on Pervasive Computing and Communications (Percom 2015), 2015.

Juan Ye, Graeme Stevenson, and Simon Dobson. KCAR: a knowledge-driven approach for concurrent activity recognition. Pervasive and Mobile Computing, 19:47–70, 2015.

Juan Ye, Graeme Stevenson, and Simon Dobson. Using temporal correlation and time series to detect missing activity-driven sensor events. In Proc. of the 11th Workshop on Context and Activity Modelling and Recognition (CoMoRea’15), 2015.

Weiren Yu and Julie A. McCann. Effectively Positioning Water Loss Event in Smart Water Networks. In Proc. of the 2nd Int. Electronic Conference on Sensors and Applications, 2015.

Franco Zambonelli, Andrea Omicini, Bernhard Anzengruber, Gabriella Castelli, Francesco DeAngelis, Giovanna di Marzo Serugendo, Simon Dobson, Jos ́e-Luis Fernandez Marquez, Alois Ferscha, Marco Mamei, Stefano Mariani, Ambra Molesini, Sara Montagna, Jussi Nieminen, Danilo Pianini, Alberto Rosi, Graeme Stevenson, Mirko Viroli, and Juan Ye. Developing pervasive multiagent systems with nature-inspired coordination. Pervasive and Mobile Computing, 17:236–252, 2015.

2014

Usman Adeel, Shusen Yang, and Julie A. McCann. Self-Optimizing Citizen-Centric Mobile Urban Sensing Systems. In Xiaoyun Zhu, Giuliano Casale, and Xiaohui Gu, editors, Proc. of the 11th International Conference on Autonomic Computing (ICAC’14), pages 161–167. USENIX Association, 2014.

Oana Andrei, Muffy Calder, Matthew Higgs, and Mark Girolami. Probabilistic Model Checking of DTMC Models of User Activity Patterns. In Gethin Norman and William H. Sanders, editors, Proc. of the 11th Conference on Quantitative Evaluation of Systems (QEST’14), volume 8657 of Lecture Notes in Computer Science, pages 138–153. Springer, 2014.

Muffy Calder, Alexandros Koliousis, Michele Sevegnani, and Joseph S. Sventek. Real-time verification of wireless home networks using bigraphs with sharing. Sci. Comput. Program., 80:288–310, 2014.

Muffy Calder and Michele Sevegnani. Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing. Formal Asp. Comput., 26(3):537– 561, 2014.

Louise A. Dennis, Michael Fisher, Nicholas Lincoln, Alexei Lisitsa, and Sandor M. Veres. Practical Verification of Decision-Making in Agent-Based Autonomous Systems. Automated Software Engineering, pages 1–55, 2014.

Lei Fang and Simon Dobson. Data collection with in-network fault detection based on spatial correlation. In Proc. of the International Conference on Cloud and Autonomic Computing (CAC'14), 2014.

Abu Raihan M. Kamal, Chris Bleakley, and Simon Dobson. Failure detection in wireless sensor networks: a sequence based dynamic approach. ACM Transactions on Sensor Networks, 10(2), 2014.

Sokratis Kartakis and Julie A. McCann. Real-time Edge Analytics for Cyber Physical Systems using Compression Rates. In Xiaoyun Zhu, Giuliano Casale, and Xiaohui Gu, editors, Proc. of the 11th International Conference on Autonomic Computing (ICAC’14), pages 153–159. USENIX Association, 2014.

Roman Kolcun and Julie A. McCann. Dragon: Data discovery and collection architecture for distributed IoT. In Proc. of the 4th International Conference on the Internet of Things (IOT’14), pages 91–96. IEEE, 2014.

Savas Konur, Michael Fisher, Simon Dobson, and Stephen Knox. Formal verification of a pervasive messaging system. Formal Asp. Comput., 26(4):677–694, 2014.

M.A. Razzaque and Simon Dobson. Energy efficient sensing in wireless sensor networks using compressed sensing. Sensors, 14(2):2822–2859, 2014.

Shusen Yang and Julie A. McCann. Distributed Optimal Lexicographic Max-Min Rate Allocation in Solar-Powered Wireless Sensor Networks. TOSN, 11(1):9:1– 9:35, 2014.

Juan Ye, Graeme Stevenson, and Simon Dobson. USMART: an unsupervised semantic mining activity recognition technique. ACM Transactions on Intelligent Interaction Systems, 4(4), 2014.

2013

Lei Fang and Simon Dobson. Unifying sensor fault detection with energy conservation. In Proc. of the 7th International Workshop on Self-Organising Systems (IWSOS’13), 2013.

Lei Fang, Simon Dobson, and Danny Hughes. An error-free data collection method exploiting hierarchical physical models of wireless sensor networks. In Proc. of the Tenth ACM International Symposium on Performance Evaluation of Wireless Ad Hoc, Sensor, and Ubiquitous Networks. ACM Press, 2013.

Michael Fisher, Louise A. Dennis, and Matthew P. Webster. Verifying autonomous systems. Commun. ACM, 56(9):84–93, 2013.

Savas Konur, Michael Fisher, and Sven Schewe. Combined model checking for temporal, probabilistic, and real-time logics. Theor. Comput. Sci., 503:61–88, 2013.