Presenter: Naghmeh Ghafari, Research Associate, Critical Systems Labs
Location: Room 239 in Building NE1 - BCIT Burnaby Campus, 3700 Willingdon Ave, Burnaby (Directions)
Abstract:
In this presentation, I describe a collaborative effort in which formal method is being used to verify properties of a structure within the Large Hadron Collider (LHC) machine protection system at the European Organization for Nuclear Research (CERN).
This structure, known as Successive Running Sums (SRS), generates the primary input to the decision logic that must initiate a critical action by the LHC machine protection system in response to the detection of a dangerous level of beam particle loss. Our formal verification effort uses mechanized logical deduction, or theorem proving. In general, theorem proving is used to show that desired properties of a system are logically implied by a formal model of the system. The use of mechanized logical deduction complements an intensive study of the SRS structure using testing and simulation. We are especially interested in using logical deduction to obtain a generic result that will be applicable to variants of the SRS structure.
This collaborative effort has individuals with diverse backgrounds ranging from theoretical physics to system safety. The use of a formal method has compelled the stakeholders to clarify intricate details of the SRS structure and behaviour.
About Naghmeh Ghafari:
Naghmeh Ghafari earned a Ph.D. (2009) in Computer Science and a M.A.Sc. (2003) in Computer Engineering from the University of Waterloo, Ontario, and a B.Sc. (2000) in Electrical Engineering from the University of Tehran, Iran.
Naghmeh's experience includes seven years as Research Assistant and four years as Teaching Assistant at the University of Waterloo. She has been an instructor for Software Requirements course at the University of British Columbia. Her research interests are in software engineering, in particular, formal verification of software systems. Currently, she is a research associate at Critical Systems Labs Inc. (CSL) working on developing formal specification and verification techniques for safety critical systems. Prior to joining CSL, she was a postdoctoral fellow at the University of British Columbia. She is a recipient of the NSERC Doctorate Scholarship and NSERC Industrial R&D Fellowship.
The meeting will start at 6:45pm. However, we advise attendants to arrive between 6:00pm and 6:45pm to enjoy refreshments, and to get acquainted with other participants.
Agenda:
- Networking before presentation
- Feature presentation
- Group discussion with the presenter
Expected duration: 2 hours.
In order to estimate the number of participants attending this event, RSVP Ed Dahl at ed.dahl@telus.net.