Abstract 1: Real-time logic (RTL) is useful for the verification of a safety assertion with respect to the specification of a real-time system. Since the satisfiability problem for RTL is undecidable, the systematic debugging of a real-time system appears impossible. With RTL, each propositional formula corresponds to a verification condition. The number of truth assignments of a propositional formula can help us determine the specific constraints which should be added or modified to derive the expected solutions. This talk describes this debugging approach and how it can be embedded into autonomous systems. We have implemented a tool called ADRTL for automatic debugging of RTL specifications. The confidence of our approach is high as we have effectively evaluated ADRTL on several existing industrial applications, including the NASA X-38 Crew Return Vehicle avionics. Abstract 2: Embedded systems are becoming ubiquitous and are increasingly interconnected or networked, making them more vulnerable to security attacks. A large class of these systems such as SCADA and PCS has real-time and safety constraints. Therefore, in addition to satisfying these requirements, achieving system security emerges as a critical challenge to ensure that users can trust these embedded systems to perform correct operations. One objective in a secure system is to identify attacks by detecting anomalous system behaviors. This part of the talk describes the challenges in the design and implementation of such intrusion detection system (IDS), addressing (1) accuracy: the IDS identifies no or as few false positives as the resource (time, space, power, etc.) and/or policy constraints allow, and no or as few false negatives as the resource and/or policy constraints allow; (2) efficiency/timeliness: the IDS does not violate the host embedded system's application deadlines and has a reasonable space overhead; (3) scalability: the IDS can scale to work with large embedded systems; and (4) power-awareness: the IDS does not significantly reduce the operational period of battery-powered embedded systems. We conclude with an outline of one of several promising embedded IDS approaches under investigation. This approach is based on automatic rule-base generation and semantic analysis.
View all episodes
