Education Class 2

Title: A synchronous approach for the design of biomedical cyber-physical systems
Instructor: Partha Roop, University of Auckland

Abstract: Many biomedical systems use embedded controllers to control physical processes, and consequently form a class of Cyber-Physical Systems (CPSs). Examples range from pacemakers to automated insulin pumps. These systems must work safely at all times. In this tutorial, we will focus on a design methodology for such CPSs.

We rely on the well-known synchronous approach for modelling the biological processes i.e. the human organ in question at a suitable abstraction-level as well as the medical device. Using the synchronous approach helps in both modelling and verification as well as automated code generation. The synchronous approach provides well known benefits such as deterministic execution, which is an ideal fit for ensuring safety. This tutorial will introduce a systematic design approach starting with modelling of biomedical devices using the SCCharts synchronous language. Next, the Intel NIOS II platform will be introduced as a means of prototyping a given medical device. This prototype device can then be run in closed-loop with a real-time version of the associated human organ. We will use a cardiac pacemaker as a running example and will therefore briefly introduce modelling of the cardiac conduction system using compositional models. We will then demonstrate how the pacemaker can be tested, in closed-loop, with the adjoining model of the cardiac conduction system. Additionally, we will present an approach for the formal verification of this device, using the tool UPPAAL and associated properties to ensure its correct operation. We will also present how pacemakers can be secured in the face of adversarial attacks, before presenting key areas for future research.

Bio: Partha’s research interests are in Digital Health, Formal Methods for Safety-Critical applications of AI and Machine Learning, and Real-Time Systems. Partha is working with colleagues from the Medical School and the Auckland Bioengineering Institute (ABI) on new techniques developed by his group known as organ on a chip. He is also interested in heart rate variability and Biofeedback.

Partha is an academic in the Department of Electrical and Computer Engineering (http://www.ece.auckland.ac.nz/) at the University of Auckland (http://www.auckland.ac.nz/). He is currently the Associate Dean (International) for the Faculty of Engineering.

He completed his PhD in Computer Science and Engineering at the University of New South Wales, Sydney, Australia (http://www.cse.unsw.edu.au/), a M.Tech at Indian Institute of Technology in Kharagpur, India (http://www.iitkgp.ac.in/departments/home.php?deptcode=CS) and a BE degree at Anna University (College of Engineering), Madras, India (http://www.annauniv.edu/). Partha had visiting positions in Kiel University, Germany (collaboration with the Embedded Systems Group: http://www.informatik.uni-kiel.de/en/rtsys/ (http://www.informatik.uni-kiel.de/en/rtsys/), French National Laboratory of Informatics and Control (SPADES team Grenoble: https://team.inria.fr/spades/ (https://team.inria.fr/spades/)), and Iowa State University (http://www.ece.iastate.edu (http://www.ece.iastate.edu)). He collaborates with University of California, Berkeley in the PRET project: http://chess.eecs.berkeley.edu/pret/ (http://chess.eecs.berkeley.edu/pret/).

He heads the precision timed systems research group: http://homepages.engineering.auckland.ac.nz/~pretzel/ (http://homepages.engineering.auckland.ac.nz/~pretzel/). His group has created a tool-chin for the design of automation and embedded systems using the IEC61499 standard. The tool and associated benchmarks are available for download from: http://timeme.io (http://timeme.io). [https://apimatic.io/img/logo.png]

Partha co-founded APIMatic (https://apimatic.io), a cloud services company for automatic SDK generation using the model-driven approach. He has co-authored two research monographs:

– Model-Driven Design Using IEC 61499: A Synchronous Approach for Embedded and Automation Systems (2015): http://link.springer.com/book/10.1007%2F978-3-319-10521-5 (http://link.springer.com/book/10.1007%2F978-3-319-10521-5)
– Correct-by-Construction Approaches for SoC Design (2013): http://link.springer.com/book/10.1007/978-1-4614-7864-5 (http://link.springer.com/book/10.1007/978-1-4614-7864-5)