w Teesside University - Computing, Media & the Arts research - Machine Intelligence Research Group

Software and Systems Research Group

Overview

The research within the Software and Systems Research Group covers a wide range of topics in Computer Science. Our areas of work include programming theories and semantics, formal specification and verification, specialised/advanced program logics, program analysis and refinement, interactive theorem proving, reversible computing, internet of things and cyber-physical systems.

The aim and vision of our research is to enable and support the construction of reliable, safe, and secure software and systems. For this, we apply mathematically-founded techniques to the specification, modelling, verification and validation of software and systems. We are also keen to work closely with industrial partners to support the design and implementation of intelligent and reliable software and systems via knowledge transfer partnerships or consultancy. Our research also has strong connection and involvement with Teesside University Grand Challenge themes such as Resilient and Secure Societies, Digital and Creative Economy.

Our group can be linked to research groups/centres in other schools, such as the Healthcare Innovation Centre (SoHSC), Smart Energy Systems Research Group (SSED), and Centre of Crime, Harm Prevention and Security (SSSHL).

Research Activities and Current Projects

Recent research within the group includes:

  • Concurrency and weak memory in programming languages
  • Programming methodologies and paradigms, with particular emphasis on object orientation and reversible computing
  • Cyber-physical systems for smart working and living environment
  • Intelligent Internet of things
  • Software security, focused on formal verification and certified programming

Current projects:

  • “Privacy server user interface prototype development: With nested feasibility evaluation” (2018-2019), funded by Information Commissioner’s Office (ICO) (£82,444) (PI: Jim Longstaff, Co-I: Denis Martin)

Previous Projects

  • "Review: an Innovative Intelligent Evidence Exploration System" (2015--2017). Knowledge Transfer Partnership. Co-funded by Innovate UK (£147,354) (J. F. Ferreira)
  • "Safe hybrid critical systems via automated testing from formal user requirements" (2015-2017). Knowledge Transfer Partnership. Co-funded by Innovate UK (£108,324) (J. F. Ferreira)
  • "Inference Mechanisms for a Separation and Numerical Domain" (10. 2009 - 9. 2013). EPSRC funded project. Total value: £488,899 (RC contribution: £ 403,535) (S. Qin)

Staff Members

  • Usman Adeel
  • Yingke Chen
  • João F. Ferreira
  • Mengda He
  • Quang Loc Le
  • Jim Longstaff
  • Alexandra Mendes
  • Chunyan Mu
  • Shengchao Qin
  • Mohammad Abdur Razzaque
  • Bo Wei

PhD Students

  • Saul Johnson (Graduate Tutor with João F. Ferreira and Alexandra Mendes): Verification Techniques for Software Security, 2017 -
  • Chris Curry (Graduate Tutor with Quang Loc Le and Shengchao Qin): Software Verification for Cybersecurity, 2018 -
  • Chidimma Opara (with Bo Wei, Biju Issac and Shengchao Qin): Secure Cyber Physical Systems, 2018 -

Selected Publications

Post-REF 2014

  • A. Mendes and J. F. Ferreira. Towards Verified Handwritten Calculational Proofs (short paper). In the 9th International Conference on Interactive Theorem Proving, 2018
  • C. Mu, P. Dittrich, D Parker, J. E. Rowe. Organisation-Oriented Coarse Graining and Refinement of Stochastic Reaction Networks. IEEE/ACM Transactions on Computational Biology and Bioinformatics. 2018.
  • C. Mu and S. Qin. Time-sensitive Information Flow Control in Timed Event-B,11th International Symposium on Theoretical Aspects of Software Engineering (TASE). Sophia Antipolis, France. 13-15 September 2017.
  • Q. L. Le, J. Sun, S. Qin. Frame Inference for Inductive Entailment Proofs in Separation Logic. 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018). LNCS 10805. Pages 41-60.
  • L. Shi, Y. Zhao, Y. Liu, J. Sun, J. S. Dong, and S. Qin. A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Formal Aspects of Computing. 2018.
  • M. A. Razzaque, M. T. Hira, M. Dira, QoS in Body Area Networks: A Survey. ACM Transactions on Sensor Networks, 13(3): 25:1-25:46 (2017)
  • J. F. Ferreira, S. A. Johnson, A. Mendes, P. J. Brooke. Certified Password Quality: A Case Study using Coq and Linux Pluggable Authentication Modules. In Proceedings of the 13th International Conference on integrated Formal Methods (iFM), 2017
  • A. Almohammad, J. F. Ferreira, A. Mendes, and P. White. Hierarchical Requirements Modeling and Test Generation for Industrial Control Systems. In 4th International Workshop on Requirements Engineering and Testing (RET), 2017
  • A. Lindsay, J. Read, J. F. Ferreira, T. Hayton, J. Porteous, P. J. Gregory. Framer: Planning Models from Natural Language Action Descriptions. In 27th International Conference on Automated Planning and Scheduling (ICAPS), 2017
  • J. Matthews, F. Charles, J. Porteous, A. Mendes. MISER: Mise-En-Scene Region Support for Staging Narrative Actions in Interactive Storytelling. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), 2017
  • J. Li, J. Sun, L. Li, Q. L. Le and S.-W. Lin. Automatic Loop-invariant Generation and Refinement through Selective Sampling. In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2017
  • Q. L. Le, M. Tatsuta, J. Sun and W.-N. Chin. A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic, In proceedings of 29th International Conference on Computer Aided Verification (CAV), 2017
  • M. He, V. Vafeiadis, S. Qin and J. F. Ferreira, GPS+: Reasoning about Fences and Relaxed Atomics, International Journal of Parallel Programming, 2017
  • S. Qin, G. He, W.-N. Chin, F. Craciun, M. He, Z. Ming, Automated specification inference in a combined domain via user-defined predicates, Science of Computer Programming, Vol 148, 189-212, 2017
  • C. Huang, X. Chen, Y. Zhang, S. Qin, Y. Zeng, X. Li. Switched Linear Multi-Robot Navigation Using Hierarchical Model Predictive Control. International Joint Conference on Artificial Intelligence (IJCAI-17). Melbourne. 19-25th August 2017
  • R. Banach, M. Butler, S. Qin, H. Zhu. Core Hybrid Event-B II: Multiple Cooperating Hybrid Event-B Machines. Science of Computer Programming. 139:1-35 (2017). Elsevier.
  • X. Wang, J. Sun, T. Wang, S. Qin. Language Inclusion Checking of Timed Automata with Non-Zenoness. IEEE Transactions on Software Engineering. 43(11): 995-1008. 2017.
  • B. Chen, S. Yu, J. Tang, M. He, Y. Zeng, Using function approximation for personalized point-of-interest recommendation", Expert Systems with Applications, Vol 79, 225-235, 2017
  • E. Sonu, Y. Chen, P. Doshi, Decision-Theoretic Planning Under Anonymity in Agent Populations. Journal of Artificial Intelligence Research, 59: 725-770, 2017
  • M. Chandrasekaran, Y. Chen, P. Doshi, On Markov Games Played by Bayesian and Boundedly-Rational Players, AAAI, 437-443, 2017
  • Y. Shen, W. Hu, M. Yang, B. Wei, S. Lucey, C. T. Chou, Learn to Recognise: Exploring Priors of Sparse Face Recognition on Smartphones, IEEE Transaction on Mobile Computing, 16(6), 2017
  • C. Mu, P. Dittrich, D Parker, J. E. Rowe. Formal Quantitative Analysis of Reaction Networks Using Chemical Organisation Theory, 14th International Conference Computational Methods in Systems Biology (CMSB), 2016.
  • M. A. Razzaque, M. Milojevic-Jevric, A. Palade, S. Clarke, Middleware for Internet of Things: A Survey. IEEE Internet of Things Journal 3(1): 70-95 2016
  • C. Huang, X. Chen, Y. Zhang, S. Qin, Y. Zeng, X. Li, Hierarchical Model Predictive Control for Navigation of Multi-Robot Systems, International Joint Conference on Artificial Intelligence (IJCAI), 2016
  • M. He, V. Vafeiadis, S. Qin, J. F. Ferreira. Reasoning about Fences and Relaxed Atomics. 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), 520-527, 2016
  • Q. L. Le, J. Sun and W.-N. Chin, Satisfiability Modulo Heap-Based Programs, In proceedings of 28th International Conference on Computer Aided Verification (CAV), 2016
  • M. Tatsuta, Q. L. Le and W.-N. Chin, Decision Procedure for Separation Logic with Inductive Predicates and Presburger Arithmetic. In Proceedings of 14th Asian Symposium on Programming Languages and Systems (APLAS), 2016.
  • Y. Zeng, P. Doshi, Y. Chen, Y. Pan, H. Mao, M. Chandrasekaran, Approximating behavioral equivalence for scaling solutions of I-DIDs, Knowledge and Information Systems, 49(2): 511-552, 2016
  • H. Mao, Y. Chen, M. Jaeger, T. D. Nielsen, K. G. Larsen, B. Nielsen, Learning deterministic probabilistic automata from a model checking perspective, Machine Learning, 105(2):255-299, 2016
  • Y. Shen, W. Hu, M. Yang, J. Liu, Bo Wei, S. Lucey, C. T. Chou, Efficient and Robust Compressive Background Subtraction, IEEE Transaction on Mobile Computing, 15(2), 2016
  • M. A. Razzaque, S. S. Javadi, Y. C., M. T. Hira, QoS-Aware Error Recovery in Wireless Body Sensor Networks Using Adaptive Network Coding. Sensors 15(1): 440-464, 2015
  • T. C. Le, S. Qin and W.-N. Chin. Termination and non-termination specification inference. The 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 489-498, 2015.
  • R. Banach, M. Butler, S. Qin, N. Verma, and H. Zhu. Core Hybrid Event-B I: Single Hybrid Event-B machines. Science of Computer Programming. 105:92–123 (2015).
  • H. Zhu, J. He, S. Qin, P. J. Brooke. Denotational semantics and its algebraic derivation for an event-driven system-level language. Formal Aspects of Computing. 27(1): 133-166 (2015).
  • J. F. Ferreira and A. Mendes. A calculational approach to path-based properties of the Eisenstein–Stern and Stern–Brocot trees via matrix algebra. Journal of Logical and Algebraic Methods in Programming, In Press, December 2015.
  • J. Sun, H. Xiao, Y. Liu, S.-W. Lin and S. Qin. TLV: abstraction through testing, learning, and validation. The Joint Meeting of ACM SIGSOFT Symposium on the Foundations of Software Engineering and the European Software Engineering Conference (FSE/ESEC 2015). Bergamo, Italy. 2-4 Sep 2015.
  • E. Sonu, Y. Chen, P. Doshi, Individual Planning in Agent Populations: Exploiting Anonymity and Frame-Action Hypergraphs, ICAPS, 202-210, 2015
  • Y. Chen, P. Doshi, Y. Zeng, Iterative Online Planning in Multiagent Settings with Limited Model Spaces and PAC Guarantees, AAMAS, 1161-1169, 2015
  • B. Wei, A. Varshney, N. Patwari, W. Hu, T. Voigt, C. T. Chou, dRTI: Directional Radio Tomographic Imaging, In proceedings of the 14th ACM/IEEE Conference on Information Processing in Sensor Networks (IPSN), 2015
  • B. Wei, W. Hu, M. Yang, C. T. Chou, Radio-based Device-free Activity Recognition with Radio Frequency Interference, In proceedings of the 14th ACM/IEEE Conference on Information Processing in Sensor Networks (IPSN), 2015
  • E. Asarin, M. Bockelet, A. Degorre, C. Dima and C. Mu. Asymptotic behaviour in temporal logic, Joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS), Jul. 2014
  • M. A. Adnan, M. A. Razzaque, I. Ahmed, I. F. Isnin, Bio-Mimic Optimization Strategies in Wireless Sensor Networks: A Survey. Sensors 14(1): 299-345, 2014
  • M. A. Razzaque, S. Dobson, Energy-Efficient Sensing in Wireless Sensor Networks Using Compressed Sensing. Sensors 14(2): 2822-2859, 2014
  • F. Doroodgar, M. A. Razzaque, I. F. Isnin, Seluge++: A Secure Over-the-Air Programming Scheme in Wireless Sensor Networks. Sensors 14(3): 5004-5040, 2014
  • Q. L. Le, C. Gherghina, S. Qin and W.-N. Chin. Shape Analysis via Second-Order Bi-Abduction. 26th International Conference on Computer Aided Verification (CAV 2014). LNCS 8559. Pages:52-68. July 18-22, 2014. Vienna, Austria.
  • S. Qin, G. He, C. Luo, W.-N. Chin, and H. Yang. Automatically refining partial specifications for heap-manipulating programs. Science of Computer Programming. 82 (2014):56-76. Elsevier.
  • J. F. Ferreira, C. Gherghina, G. He, S. Qin and W.-N. Chin. Automated verification of the FreeRTOS scheduler in Hip/Sleek. International Journal on Software Tools for Technology Transfer, 16(4):381-397. Springer. 2014.
  • A. Mendes, R. C. Backhouse, J. F. Ferreira. Structure Editing of Handwritten Mathematics: Improving the Computer Support for the Calculational Method. ITS 2014: 139-148.
  • Y. Shen, W. Hu, M. Yang, B. Wei, S. Lucey, C. T. Chou, Face Recognition on Smartphones Via Optimised Sparse Representation Classification, In proceedings of the 13th ACM/IEEE Conference on Information Processing in Sensor Networks (IPSN), 2014