Abstracts
of Selected RTS Group Publications
- 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