The talk will address the formal development of Cyber-Physical Systems, which include both discrete and continuous behaviours.
Watch the video
Download the presentation slides (PDF)
Synopsis
Cyber-physical systems (CPS) are complex computer-based systems which have closely intertwined physical processes, computation and networking system aspects. Some of their development and safety assurance difficulties arise from the need to model and reason at a system-level, and hybrid behaviours which are best captured by hybrid automata models. In this seminar I will present a formal development approach of cyber-physical systems using the Event-B formal method which is based upon refinement and proof-based verification. To improve the level of automation in the deductive verification of the resulting hybridised Event-B CPS models, the seminar will describe an approach of integrating reachability analysis in the proof process.
About the speaker
Paulius Stankaitis
Paulius Stankaitis is a Research Associate at Newcastle University where he is part of the Advanced Model-Based Engineering and Reasoning (AMBER) research group. He received PhD from Newcastle University on the topic of formal modelling and verification of heterogeneous railway signalling systems. His current research focuses on integrating different formal verification methods for reasoning about safety of cyber-physical and autonomous systems.
Our events are for adults aged 16 years and over.
BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today
This event is brought to you by: FACS (Formal Aspects of Computing Science) group
