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.
cited By (since 1996)0; Conference of org.apache.xalan.xsltc.dom.DOMAdapter@5194c830 ; Conference Date: org.apache.xalan.xsltc.dom.DOMAdapter@7ee2f127 Through org.apache.xalan.xsltc.dom.DOMAdapter@65467885; Conference Code:97500
Jayaraj Poroor and Jayaraman, Bb, “Formal analysis of event-driven cyber physical systems”, in ACM International Conference Proceeding Series, Kerala, 2012, pp. 1-8.