|
|
 |
|
NIA Formal Methods Seminar by Borzoo Bonakdarpour |
|
Date: May 8, 2006
Time: 10:30am
Location: NIA, Rm 137
Additional Information: Presentation (PDF)
Automated Revision of Existing Real-Time Programs
Borzoo Bonakdarpour, Michigan State University
Automatic revision of existing real-time programs is the problem of adding properties (to programs) that are later discovered as a crucial part of the program. Since the existing synthesis algorithms are highly complex, we characterize a class of real-time programs and properties, where adding properties to programs is practically feasible in the sense that the time and space complexity of synthesis algorithms are comparable to that of existing model checking techniques in the dense real-time model.
We focus on this problem in two contexts. First, we investigate the problem of automated addition of properties expressed in Metric Temporal Logic (MTL) formulas to existing real-time programs modeled in Alur and Dill timed automata. In particular, we devise synthesis algorithms or hardness results for adding different types of time-bounded liveness properties to real-time program.
Second, we concentrate on transformation algorithms, where we design synthesis methods to add fault-tolerance to existing fault-intolerant real-time programs. To this end, we first develop a formal framework independent of platform and architecture to define the notions of faults and fault-tolerance in the context of real-time programs. We consider three levels of fault-tolerance (namely, failsafe, nonmasking, and masking) based on satisfaction of safety and liveness properties in the presence of faults. Furthermore, we propose two additional levels of fault-tolerance (namely, soft and hard) based on satisfaction of timing constraints in the presence of faults. Using this framework, we devise synthesis algorithms for adding different levels of fault-tolerance to existing real-time programs.
|
|
|
Home