	Real-Time Systems Group

Introduction

The Real-Time Systems research group is headed by Prof. Aloysius Mok. In the past few years, we have worked towards laying the groundwork for establishing a firm theoretical foundation for real-time systems and also to build design tools based on this foundation. Our work can be categorized into three areas as follows:

Specification and Modeling: precise formulation of real-time properties of systems.
Analysis and Verification: reasoning about real-time properties.
Synthesis: enforcing stringent timing constraints and other real-time properties.

Current Projects

WirelessHART

Wireless technology has been regarded as a paradigm shifter in the process industry. The first open wireless communication standard specifically designed for process measurement and control applications, WirelessHART was officially released in September 2007 (as a part of the HART 7 Specification) by the HART Communication Foundation. WirelessHART is a secure and TDMA-based wireless mesh networking technology operating in the 2.4 GHz ISM radio band. Now, we are trying to build a WirelessHART protocol stack for it.

Software Verification

Model-based development has been recognized as a practical method for efficiently developing correct and robust control-oriented real-time embedded systems.Generally model-based development has focused on verification and testing for functional or timeliness aspects. However, embedded software also involves para-functional resource-related aspects, termed resource(bound) properties.Yet verification and testing for such resource properties has been rarely addressed in executable model-based development. Resource-related language constructs are not incorporated in the action semantics of executable models since early design is intended to be platform independent. Here, we propose a software engineering discipline which incorporates resource safety verification into a design and development methodology for embedded systems .

Real-time Non-Preemptive Scheduling

Unlike preemptive scheduling policies, non-preemptive real-time scheduling policies can exhibit anomalies even for the single-processor case. In particular, a task set that is schedulable by a non-preemptive scheduler may become unschedulable when the utilization of the task set decreases relative to the CPU speed, e.g., when a faster CPU is used to run the same task set. We define the notion of robustness to capture the essence of the scheduling anomaly on real-time system performance. We shall show that it is difficult to test for robustness in general but there are sufficient conditions for guaranteeing robustness.

Real-time introsion prevention

The use of automatic signature generators (ASGs) as a defense against fast propagating, zero-day worms has received a lot of attention lately, and various attacks against these systems are also being discovered. Allergy attack is one of these attacks. Some ASGs employ some form of corpus-based mechanisms to retrofit for a low false positive rate. We shall show that corpus-based mechanisms are not a general solution against allergy attacks. In particular, we will identify two major weaknesses of a corpus-based defense and present advanced allergy attacks that exploit them.

Current Members