Back close

Formal analysis of event-driven cyber physical systems

Publication Type : Conference Paper

Thematic Areas : Amrita Center for Cybersecurity Systems and Networks

Publisher : ACM International Conference Proceeding Series

Source : ACM International Conference Proceeding Series, Kerala, p.1-8 (2012)

Url :

ISBN : 9781450318228

Keywords : ACM proceedings, Compositional verification, Cyber physical systems (CPSs), Embedded systems, Explosions, Formal analysis, Formal Verification of Security, Internet, Latexes, Model checking, Physical systems, Security of data, Specifications, State explosion, Text tagging, Theorem proving

Campus : Amritapuri

School : Centre for Cybersecurity Systems and Networks, School of Engineering

Center : Cyber Security

Department : Computer Science, cyber Security

Year : 2012

Abstract : We propose a programming language (E#) that facilitates formal verification of security properties of event-driven cy- berphysical systems. We describe the syntax of E# with the help of several illustrative examples. Since the environment plays a crucial role in cyberphysical systems, E# facilitates modeling of the environment processes abstractly using the novel 'causes' clauses. We show that event causality graphs (ECGs) may be constructed from causes clauses and handle specifications. We present how ECGs can be used to detect compute-bound event loops which are undesirable in event- driven systems and also to analyze response-style event live- ness specifications. We show how safety properties can be inductively established by employing either theorem-proving or model checking. This technique facilitates compositional verification, allowing us to establish properties of each component separately. The technique also avoids state explosion that arises due to interleaving of the atomic blocks of concurrent event handlers. An interesting feature of our safety analysis is our use of model checking for safety properties in an inductive setting. We conclude that E# is a viable language for programming safety-critical event-driven cyber- physical systems. Copyright 2012 ACM.

Cite this Research Publication : Jayaraj Poroor and Jayaraman, Bb, “Formal analysis of event-driven cyber physical systems”, in ACM International Conference Proceeding Series, Kerala, 2012, pp. 1-8.

Admissions Apply Now