- Detecting Unknown Massive Mailing Viruses Using Proactive Methods,
by Ruiqi Hu and Aloysius K. Mok.
UTCS Technical Report RTS-TR-04-01.

The detection of unknown viruses is beyond the capability of many existing virus detection approaches. In this paper, we show how proactive customization of system behaviors can be used to improve the detection rate of unknown malicious executables. Two general proactive methods, behavior skewing and cordoning, and their application in BESIDES, a prototype system that detects unknown massive mailing viruses, are presented.

- A Hybrid Proactive Approach for Integrating Off-line and On-line Real-Time Schedulers,
by Weirong Wang, Aloysius K. Mok and Gerhard Fohler.
UTCS Technical Report RTS-TR-03-01.

The issue of integrating event-driven workload into existing static schedules has been addressed by Fohler's Slot Shifting method. Slot Shifting takes a static schedule for a time-driven workload as input, analyzes its slacks off-line, and makes use of the slacks to accommodate an event-driven workload on-line. Slot Shifting is a reactive method in the sense that it does not address how to produce a static schedule so that it can be successfully integrated with the event-driven workload. We shall show that the choice of the static schedule cannot be considered independent of the event-driven workload. We propose a proactive hybrid scheduler with both an off-line component and an on-line component. Time-driven workload and event-driven workload are modeled as periodic tasks and sporadic tasks respectively. The off-line component produces a pre-schedule. The on-line component schedules all periodic and sporadic jobs by using a variation of the EDF scheduler with one additional constraint: the sequencing of the periodic jobs in the static schedule must be as specified by the pre-schedule. The off-line component is optimal in the sense that it produces a valid pre-schedule for a given periodic task set and a given sporadic task set if and only if one exists.

- Pre-Scheduling: Balancing Between Static and Dynamic Schedulers,
by Weirong Wang, Aloysius K. Mok,
UTCS Technical Report RTS-TR-02-01.

Compared with dynamic schedulers, static schedulers require lower on-line scheduling costs but higher demand on resources in capacity planning, especially if there are sporadic tasks whose deadlines are relatively short compared with their mean interval of arrival. An hybrid scheduling approach is proposed in this paper to strike a balance between static and dynamic schedulers in a real-time system with both periodic and sporadic tasks. The hybrid approach is based on the technique we call pre-scheduling. Like a static schedule, a pre-schedule of periodic tasks is produced off-line but unlike a static schedule, a pre-schedule has built in slack for the periodic tasks so that their start-times are not fixed. Pre-schedules are used on-line with two on-line schedulers. A dynamic on-line scheduler schedules sporadic tasks at high priority, and a static on-line scheduler schedules the periodic tasks according to the pre-schedule at low priority. The chanllenge of this approach is that the arrival times of sporadic tasks are not known \emph{a priori}, yet a pre-schedule must be produced off-line to make sure that a valid schedule is always produced by the on-line schedulers. In this paper, this chanllenge is answered with an optimal and computationally practical pre-scheduler. The pre-scheduling approach augments and extends the capability of architectures such as TTA (Time Triggered Architecture).

- Formal Specification of Real-Time Systems, by
Farnam Jahanian, Aloysius K. Mok and Douglas A. Stuart, UTCS Technical
Report UTCS-TR-88-25.

This paper presents the formal syntax and semantics of*Real Time Logic (RTL)*, a logic for the specification of real-time systems. An example illustrating the specification of a system in RTL is presented, and natural deduction is used to verify that the system satisfies a given safety property. RTL is shown to be undecidable by a reduction from the acceptance problem for two-counter machines. Decidable subclasses of the logic are also discussed.

- Compiling Modechart Specifications, by Carlos
Puchol, Aloysius K. Mok and Douglas A. Stuart, in Proc. IEEE Real-Time
Systems Syposium '95.

The Modechart specification language is a formalism for the specification of real-time systems. A toolset for specification, analysis and simulation for Modechart specifications exists for supporting the design and construction of real-time systems. This paper introduces a new tool in the the toolset: a compiler for a class of Modechart specifications, namely, that of deterministic system specifications, extended by a subclass of the non-deterministic system specifications. The object code that the compiler generates is in Esterel, a member of the synchronous family of programming languages for real-time systems. We discuss a broad approach to the implementation of timing specifications, providing a range of implementation options, from the basic time step unrolling of states in Esterel, to the use of system timers. The compiler presented herein allows the specifier to obtain a correct implementation of a modechart program, including timing constraints.

- A Methodology and Support Tools for Analysis of
Real-Time Specifications, by Douglas A. Stuart, Aloysius K. Mok, Farnam
Jahanian.

As software control of time-critical functions in*embedded systems*becomes more common, a means for the precise specification of their behavior and formal methods for analyzing system requirements becomes increasingly important. Modechart is a graphical specification language introduced to meet this need. The main focus of paper is on methods and supporting tools for representing and reasoning about properties of time-critical systems specified in Modechart. The paper describes a verification methodology which takes advantage of the structuring inherent in a Modechart specification to determine whether a system specification satisfies the required properties. The paper also describes the implementation of a*mechanical verifier*based on the proposed approach, which has been recently integrated as part of the Modechart Toolset prototype development environment from the Naval Research Lab .

- A Solution to the Generalized Railroad Crossing
Problem in Esterel, by Carlos Puchol, UTCS Technical Report UTCS-TR-95-05.

We present a solution to the Generalized Railroad Crossing benchmark problem based on the Esterel programming language. The solution is shown to satisfy the formal statements of the properties that the system requirements specify by using a verification method for safety properties of Esterel programs recently developed. The solution and verification presented have been developed within the synchronous system model, i.e. discrete time, global broadcast of events and instantaneous reactions.

- Response-Time Bounds of Rule-Based Programs under
Rule Priority Structure, by R. H. Wang and A.K. Mok, in Proc. IEEE Real-Time
Systems Symposium 1994.

A key index of the performance of a rule-based program used in real-time monitoring and control is its response time, defined by the maximum number of rule firings before a fixed point of the program is reached from a start state. Previous work in computing the response-time bounds for rule-based programs assumes that if two rules are enabled, then either one of them may be scheduled for firing. This assumption may be too conservative in the case programmers choose to impose a priority structure on the set of rules. In this paper, we discuss how to get tighter bounds by taking rule-priority information into account. We show that the rule-suppression relation we previously introduced can be extended to incorporate rule-priority information. A bound-derivation algorithm for programs whose potential-trigger relations satisfy an acyclicity condition is presented, followed by its correctness proof and an analysis example.

- The Integration of Control and Dataflow Structures
in Distributed Hard Real-Time Systems, by Carlos Puchol and A. K. Mok.
International Workshop on Parallel and Distributed Real-Time Systems, WPDRTS,
1994.

The control structure of many real-time applications are naturally described by state machines. However, the state transitions of these machines are governed not only by the state of the system and the occurrence of events, but also by their time of occurrence. The control structure of a real-time system determines what computation to perform and the set of timing constraints in effect at all times. The computation performed by the system can then be modeled by a directed graph, where the nodes denote transformations on the data and the edges denote data flow. In this paper, we discuss some research issues that arise from the integration of control flow with data flow.

- Deriving Response-Time Bounds for Equational Rule-Based
Programs, by R. H. Wang and A. K. Mok, International Computer Symposium
1992.

The response time of a rule-based program is defined as the maximum number of rule firings before a fixed point of the program is reached from a start state. In this paper, we present several principles which make use of two relations, potential-trigger and suppression, for deriving tight response-time bounds. While the computation of these two relations is costly in general, we show how they can be efficiently approximated by refining the necessary/sufficient conditions for these relations to be satisfied. A response-time analyzer based on the theories in this paper has been implemented to analyze programs whose potential-trigger relations are acyclic. We demonstrate the analysis process with an example program which has infinite state space. Our analyzer takes only seconds to derive a tight bound on the example program's response time.

- A Method for Verifying Properties of Modechart
Specifications, by F. Jahanian and D. A. Stuart, in Proc. Real-Time Systems
Symposium, 1988.

As software control of time-critical functions in embedded systems becomes more common, a means for the precise specification of their behavior becomes increasingly important. Modechart is a graphical specification language introduced to meet this need. This paper presents a method for verifying properties of systems specified in Modechart. The proposed approach makes use of a computation graph which takes advantage of the structuring inherent in a Modechart specification. Two classes of properties are presented for which decision procedures are developed.

- Implementing a Verifier for Real-Time Systems, by
D. A. Stuart.

The SARTOR project has as one of its goals the development of an environment for the development of correct real-time systems. Modechart is a specification language for real-time systems developed as part of this project. Verify4 is an implementation of a verifier for certain classes of properties of systems specified using modechart. This paper describes the program verify4 and addresses implementation issues surrounding three of the key algorithms used in the program.

- A Formal Method for Verifying Real-Time Properties
of Modechart Specifications, by D. A. Stuart and F. Jahanian.

As software control of time-critical functions in embedded systems becomes more common, a means for the precise specification of their behavior becomes increasingly important. Modechart is a graphical specification language introduced to meet this need. This paper presents a method for verifying properties of systems specified in Modechart. The proposed approach makes use of a computation graph which takes advantage of the structuring inherent in a Modechart specification. Three classes of properties are presented for which decision procedures are developed.

- Syntax for Modechart ASCII files, by Paul Clements.

This paper describes the ASCII syntax of the Modechart language.

- Modechart User's Guide, by Paul Clements et. al.

This paper is the user guide for the Modechart language. [Long document: 300Kb]

Publications UT Austin RTS Group