Programs
- M. Tech. in Automotive Engineering -
- Fellowship In Interventional Pulmonology and Pulmonary Critical care - Fellowship
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)
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.