Automated Revision of Legacy Real-Time Programs:Work in Progress1Borzoo Bonakdarpour Sandeep S. KulkarniDepartment of Computer Science and EngineeringMichigan State UniversityEast Lansing, MI 48824, USAEmail: {borzoo,sandeep}@cse.msu.eduAbstractIn this paper, we focus on the problem of automatic revi-sion of legacy real-time programs. We consider this problemin two contexts. First, we investigate the problem of auto-mated addition of properties expressed in Metric TemporalLogic (MTL) formulas to existing real-time programs mod-eled in Alur and Dill timed automata. Then, we considertransformation problems, where we design synthesis meth-ods to add fault-tolerance to existing fault-intolerant real-time programs. While both problems have been addressedin the literature for untimed programs in theory and prac-tice, there is much to be done for real-time programs. Tothis end, we concentrate on filling the gap between theoryand practice of automated methods for synthesizing real-time programs by characterizing the class of real-time pro-grams and properties, where program synthesis is practi-cally feasible.Keywords: Timed automata, Real-time, Bounded live-ness, Program synthesis, Program transformation,Fault-tolerance, Formal methods.1. IntroductionAutomated program synthesis is the problem of design-ing an algorithmic method to find a program that satisfiesa required set of behaviors. Depending upon the choice offormulation of the problem and expressiveness of specifi-cations and programs, the class of complexity of synthesismethods varies from polynomial-time to undecidability.In this paper, we describe our ongoing research on auto-mated synthesis methods for revising legacy real-time pro-grams. In this research, we characterize the class of real-time programs and properties, where automated synthe-sis can be achieved efficiently and the ones that involve1 This work was partially sponsored by NSF CAREER CCR-0092724,DARPA Grant OSURS01-C-1901, ONR Grant N00014-01-1-0744,NSF grant EIA-0130724, and a grant from Michigan State Univer-sity.exponential complexities. Moreover, we study the prob-lem of revising existing real-time programs in two con-texts: (1) adding properties typically used in specifying real-time requirements to existing real-time programs, and (2)adding fault-tolerance to existing fault-intolerant real-timeprograms. Since we use the timed automata formalism [1],many real-time scheduling problems can be reduced to ourproblems as well.In the context of untimed programs, similar problemshave been addressed in the literature. In [2], the authors con-sider the problem of automated revision of legacy UNITY[3] programs. The problem of synthesizing untimed fault-tolerant programs has been studied from different perspec-tives. In [4–6], the authors propose synthesis algorithmsfor adding fault-tolerance and multitolerance to existingprograms in the high (respectively, low) atomicity model,where processes can (respectively, cannot) read and writeall the program variables in one atomic step.Synthesis of real-time programs has mostly been formu-lated in the context of timed control synthesis from gametheoretical perspective [7–12]. There are two drawbacks inthe proposed methods that make the synthesis methods ei-ther unrealistic or unfeasible: (1) the complexity of suchmethods are too high to be used in practice (at least EXP-TIME-complete), and/or (2) either the given program or thespecification must be deterministic.Organization of the paper. In Section 2, we presentthe preliminary concepts. In Section 3, we present our cur-rent results and ongoing research on adding properties tolegacy real-time programs. Then, in Section 4, we presentour current results and ongoing research on designing syn-thesis methods to add fault-tolerance to legacy real-timeprograms. In Section 5, we describe our plan to use our the-oretical results in practice. Finally, we make the concludingremarks in Section 6.2. BackgroundIn this section, we give intuitive definitions of the ter-minology that we use in this paper. A legacy real-time pro-gram is specified in terms of its state space and set of transi-tions. We use the notion of timed automata [1] to representreal-time programs. A timed automaton is a traditional fi-nite state automaton equipped with clock variables and tim-ing constraints.We model real-time properties by Metric Temporal Logic(MTL) formulas. Linear Temporal Logic (LTL) specifies thequalitative part of a program. MTL introduces real time toLTL by constraining temporal operators, so that one canspecify the quantitative part as well. For instance, the con-strained eventually operator ♦[1,3]is interpreted as “eventu-ally within 1 to 3 time units both inclusive”. A specificationis a conjunction of a set of MTL properties. A computationis an infinite sequence of states. Note that, an MTL propertydefines a set of computations. We say that a real time pro-gram P satisfies specification (or property) Σ iff all com-putations of P are in Σ. Otherwise, we say that P violatesΣ.3. Adding Properties to Legacy Real-TimeProgramsIn this section, we describe the problem of revisinglegacy real-time programs through adding new properties.Furthermore, we present our current results and ongoing re-search in this regard.Problem statement. Given are a real-time program P andan MTL property Π. Our goal is to transform P into a newreal-time program P0such that P0satisfies the given prop-erty Π and it continues to satisfy its old specification, whichis not necessarily given. Since the notion of the given property in the problemstatement can be any formula expressed in MTL, we haveto deal with a highly expressive set of properties, whichin turn (if not undecidable) requires highly complex algo-rithms. Hence, we focus on properties typically used inspecifying real-time systems rather than solving the prob-lem for any arbitrary property. More specifically, as thestarting point, we focus on the well-known time-boundedresponse property. A time-bounded response property is ofthe form Π ≡ (p → ♦≤δq), where p and q are two setsof states, and δ is a positive real number, i.e., it is alwaysthe case that a p-state is followed by a q-state within δ timeunits. One can instantiate the problem statement in the ob-vious way, i.e., our goal is to add a time-bounded responseproperty Π to an existing real-time program P.3.1. Current ResultsOur current results fall in two categories: (1) transforma-tion
View Full Document
Unlocking...