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.
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.
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.
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.
On 11 October 2018 Simon Dobson will give a keynote on "Making the transition from sensors to sensor systems software" at the Conference on Design and Architectures for Signal and Image Processing (DASIP 2018) in Porto, Portugal.
20 September 2018 All-hands meeting with invited members of the advisory board taking place at Imperial College London.
3 July 2018 Julie McCann will give the welcoming and introduction talk at the official launch of the Centre for Smart Connected Futures, a new multi-disciplinary research network at Imperial College London.
21 June 2018 Michael Fisher visited Geneva to attend a meeting of experts organised by the International Committee of the Red Cross to discuss the limits of, and issues around, autonomy in relation to autonomous weapon systems. More details here.
12 June 2018 Michele Sevegnani gave an invited talk on “Air navigation services assets management with stochastic model checking” at the “EU-China Workshop on Aviation, Air Traffic Management, Safety and Security” (part of ECCOMAS 2018) held at the University of Glasgow.
6 June 2018 Next all-hands meeting taking place in windy St Andrews.
24 April 2018 We are seeking one Postdoctoral Researcher to join the Glasgow team. More details can be found here and here. Application closing date: 22 May 2018.
6 October 2017 Prof Muffy Calder will give an invited talk at the CENSIS 4th Technology Summit and Conference 2017, which will take place in Glasgow, 2 November 2017.
5 October 2017 Our fourth all-hands meeting taking place in Manchester.
Business Development Manager
Simon Dobson, Matteo Golfarelli, Simone Graziani, and Stefano Rizzi. A reference architecture and model for sensor data warehousing. IEEE Sensors Journal, 18(18), 2018.
Michael Breza, Ivana Tomic, and Julie McCann. Failures from the Environment, a Report on the First FAILSAFE Workshop. SIGCOMM Comput. Commun. Rev., 48(2):40–45, May 2018.
I. Tomic, L. Bhatia, M. Breza, and J. A. McCann. The Limits of LoRaWAN in Event-Triggered Wireless Networked Control Systems. In Proc. of the 12th International UKACC Conference on Control, 2018.
I. Tomic, M. Breza, G. Jackson, L. Bhatia, and J. A. McCann. Design and evaluation of jamming resilient cyber-physical systems. In Proc. of the IEEE International Conference on Cyber, Physical and Social Computing (CPSCom 2018), 2018.
Ullrich Hustadt, Claudia Nalon, and Clare Dixon. Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics. In Proc. of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR’18), 2018.
Matt Webster, Michael Breza, Clare Dixon, Michael Fisher, and Julie McCann. Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems. In Proc. of the 18th International Workshop on Automated Verification of Critical Systems (AVoCS’18), 2018.
Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, and Michael Fisher. The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators. In Proc. of the 20th International Conference on Formal Engineering Methods (ICFEM’18), 2018.
Michele Sevegnani, Milan Kabac, Muffy Calder, and Julie A. McCann. Modelling and Verification of Large-Scale Sensor Network Infrastructures. In Proc. of the 23nd International Conference on Engineering of Complex Computer Systems (ICECCS), Melbourne, Australia, 2018.
Muffy Calder et al. Blackett Review: Computational Modelling. UK Government Office for Science, 2018.
Oana Andrei and Gabriel Murray. Interpreting Models of Social Group Interactions in Meetings with Probabilistic Model Checking. In Proc. of the ACM workshop ”Group Interaction Frontiers in Technology” (GIFT’18), Boulder, CO, USA, Oct 2018.
Oana Andrei and Muffy Calder. Data-driven modelling and probabilistic analysis of interactive software usage. Journal of Logical and Algebraic Methods in Programming, 100:195 – 214, 2018.
Sven Linker. Sequent Calculus for Euler Diagrams. In Peter Chapman, Gem Stapleton, Amirouche Moktefi, Sarah PerezKriz, and Francesco Bellucci, editors, Proc. of the 10th Intl. Conf. on Diagrammatic Representation and Inference (Diagrams 2018), volume 10871 of Lecture Notes in Computer Science, pages 399–407. Springer, 2018.
Muffy Calder, Claire Craig, Dave Culley, Richard de Cani, Christl A. Donnelly, Rowan Douglas, Bruce Edmonds, Jonathon Gascoigne, Nigel Gilbert, Caroline Hargrove, Derwen Hinds, David C. Lane, Dervilla Mitchell, Giles Pavey, David Robertson, Bridget Rosewell, Spencer Sherwin, Mark Walport, and Alan Wilson. Computational modelling for decision-making: where, why, what, who and how. Royal Society Open Science, 5(6), 2018.
Michael Breza and Julie A. McCann. Polite Broadcast Gossip for IOT Configuration Management. In IEEE International Conference on Smart Computing, SMARTCOMP’17, pages 1–6. IEEE Computer Society, 2017.
Paul Gainer, Clare Dixon, Kerstin Dautenhahn, Michael Fisher, Ullrich Hustadt, Joe Saunders, and Matt Webster. CRutoN: Automatic Ver- ification of a Robotic Assistant’s Behaviours. In Procs. of Joint 22nd International Workshop on Formal Methods for Industrial Critical Sys- tems (FMICS) - and - 17th International Workshop on Automated Ver- ification of Critical Systems the Critical Systems (AVoCS) 2017, pages 119–133, 2017.
Elisa Cucco, Michael Fisher, Louise Dennis, Clare Dixon, Matt Webster, Bastian Broecker, Richard Williams, Joe Collenette, Katie Atkinson, and Karl Tuyls. Towards Robots for Social Engagement. In Procs. of Workshop on Human-Robot Engagement in the Home, Workplace and Public Spaces (WHRE 2017), 2017.
Sven Linker. Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL. In Nadia Polikarpova and Steve Schneider, editors, Proc. of the 13th International Conference on Integrated Formal Methods (iFM’17), volume 10510 of Lecture Notes in Computer Science, pages 34–49. Springer, 2017.
Danilo Pianini, Simon Dobson, and Mirko Viroli. Self-stabilising target counting in wireless sensor networks using Euler integration. In Proc. of 11th International Conference on Self-Adaptive and Self-Organizing Systems (SASO’17). IEEE Computer Society, 2017.
Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, and Michael Fisher. Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking. In Nathalie Bertrand and Luca Bortolussi, editors, Proc. of 14th International Conference on Quantitative Evaluation of Systems (QEST’17), volume 10503 of Lecture Notes in Computer Science, pages 224–239. Springer, 2017.
Sven Linker and Michele Sevegnani. Formalising Sensor Topologies for Target Counting. In Danilo Pianini and Guido Salvaneschi, editors, Proc. of of 1st Workshop on Architectures, Languages and Paradigms for IoT (ALPIoT’17), volume 264 of Electronic Proceedings in Theoretical Computer Science, pages 43–57. Open Publishing Association, 2018.
Oana Andrei and Muffy Calder. Temporal Analytics for Software Usage Models. In Antonio Cerone and Marco Roveri, editors, Software Engineering and Formal Methods, volume 10729 of Lecture Notes in Computer Science, pages 9–24. Springer International Publishing, 2017.
Muffy Calder and Michele Sevegnani. Stochastic model checking for predicting component failures and service availability. IEEE Transactions on Dependable and Secure Computing, 2017.
Matt Webster, David Western, Dejanira Araiza-Illan, Clare Dixon, Kerstin Eder, Michael Fisher, and Anthony G. Pipe. An Assurance-based Approach to Verification and Validation of Human-Robot Teams. CoRR, abs/1608.07403, 2016.
Matt Webster, Clare Dixon, Michael Fisher, Maha Salem, Joe Saunders, Kheng Lee Koay, Kerstin Dautenhahn, and Joan Saez-Pons. Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study. IEEE Trans. Human-Machine Systems, 46(2):186–196, 2016.
Louise A. Dennis, Michael Fisher, Marija Slavkovik, and Matt Webster. Formal verification of ethical choices in autonomous systems. Robotics and Autonomous Systems, 77:1–14, 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.
Louise A. Dennis, Michael Fisher, and Matt Webster. Two-stage agent program verification. Journal of Logic and Computation, page exv003, 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.
Matt Webster, Clare Dixon, Michael Fisher, Maha Salem, Joe Saunders, Kheng Lee Koay, and Kerstin Dautenhahn. Formal Verification of an Autonomous Personal Robotic Assistant. In In Formal Verification and Modeling in Human-Machine Systems: Papers from the AAAI Spring Symposium (FVHMS 2014), number ISBN 978-1-57735-655-4, 2014.
Matt Webster, Clare Dixon, and Michael Fisher. Safe and Trustworthy Autonomous Robotic Assistants. Space Safety Magazine, 9, Winter 2014 2014.
Matthew P. Webster, Neil Cameron, Michael Fisher, and Mike Jump. Generating Certification Evidence for Autonomous Unmanned Aircraft Using Model Checking and Simulation. J. Aerospace Inf. Sys., 11(5):258–279, 2014.
Clare Dixon, Matthew P. Webster, Joe Saunders, Michael Fisher, and Kerstin Dautenhahn. ”The Fridge Door is Open”-Temporal Verification of a Robotic Assistant’s Behaviours (Won the Springer Award for Best Paper). In Michael Mistry, Ales Leonardis, Mark Witkowski, and Chris Melhuish, editors, Procs. of the 15th Annual Conference on Advances in Autonomous Robotics Systems (TAROS 2014), volume 8717 of Lecture Notes in Computer Science, pages 97–108. Springer, 2014.
Louise A. Dennis, Michael Fisher, Marija Slavkovik, and Matthew P. Webster. Ethical Choice in Unforeseen Circumstances. In Procs. of the 14th Annual Conference on Towards Autonomous Robotic Systems (TAROS 2013), volume 8069 of Lecture Notes in Computer Science, pages 433--445. Springer, 2013.
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.
Farshid Amirabdollahian, Kerstin Dautenhahn, Clare Dixon, Kerstin Eder, Michael Fisher, Kheng Lee Koay, Evgeni Magid, Tony Pipe, Maha Salem, Joe Saunders, and Matt Webster. Can You Trust Your Robotic Assistant? In Proc. of the 5th International Conference in Social Robotics (ICSR 2013), volume 8239 of Lecture Notes in Artificial Intelligence, pages 571--573. Springer, 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.