Specification and Error Pattern Based Program Monitoring Kla_ls Havelund I, Scott Johnson _, Grigore Ro_u :_ I Kestrel Technology, NASA Ames Research Center, USA Email: havelund@email, arc. nasa. gov " Department of Computer Science, University of Wyoming, USA Emaih skj@uwyo, edu :_BIACS, NASA Ames Research Center, USA Email: grosu @email. arc. nasa.gov Abstract We briefly present Java PathExplorer (JPAX), a tool developed at NASA Ames for monitoring the execution of Java programs../PAX can be used not only during program testing to reveal subtle errors, but also can be applied during operation to surJey safety critical systems. The tool facilitates automated instrumentation of a program in order to property observe its execution. The instrumentation can be either at the bytecode level or at the source level when the tource code is available. JPaX is an instance of a more general project, called PathExplorer (PAX), which is a basis for experiments rather than a fixed system, capable of monitoring various programming languages and ex!:erimenting with other logics and analysis techniques. 1 Introduction The success of most technological experiments today, including space craft and rover technology, heavily depends on the correctness of software. Two common ways to approach the delicate problem of software correctness are testing and formal methods. Although traditional testing techniques scale well and are by far the most used techniques in practice to v_lidate software systems, they are usually ad hoc and do not allow for formal specification and verification of high level logical properties that a system needs to satisfy. On the other hand, traditional formal methods such as model checking and theorem proving are usually very heavy and rarely can be used in practice successfully without considerable manual effort. The Automated Software Engineering group at NASA Ames Research Center has for some time investigated advanced formal methods for in,_uring software correctness, in both program synthesis [14, 5, 18] and program verification [8, 9, 17, 7, 11]. This paper, together with [10, 15, 11, 12] describes our effort in runtime verification, which can be roughly defined as combining testing and formal methods. The merge of testing and temporal logic specification is an attempt lo achieve the benefits of both approaches, while avoiding some of the pitfalls of ad hoc testing and the complexit _of theorem proving and model checking. In this paper, we present the current status of a new runtime verifica_.ion system, called Java PathExplorer (JPAX), for monitoring Java programs by analyzing (exploring) particular execution traces. We are considering two apparently distinct approaches to monitoring which can be well combined. In black-box monitoring, the general idea consists of extracting state events from an executing program, which has been automatically instrumented, and then analyzing them via an observer process. This approach is suitable in general when certain fields (variables, data structures, etc.) need to be observed at any mon:ent over the execution of the program. In white-box monitoring, one assumes that the source code of the program is available and that annotations can be introduced manually in the code at appropriate places, where they _ill then be expanded and compiled together with the program. This approach is more appropriate when certain fields need to be observed at specific places in the program. Many of the algorithms used are the same in both black-box and white-box approaches..JPAX currently performs two kinds of verification, namely logic based monitoring and error pattern analysis. Logic based monitoring consi.'ts of runtime checking formal requirement specifications written in high level logics by users of the system. Logics are currently implemented in Maude [1], a high-performance system supporting both rewriting logic and membership equational logic. One can naturally and easily define new logics in Maude, such as for exemple temporal logics, together with their finite trace operational semantics. Currently, .JPAX supports two miltin logics, future time and past time linear temporal logic. Logic based _',.rrnm,"ri.rJ,9 <:m be iz.st,a,nti;tt,e_l at, ,_it|wr r.D' _mr<e <:o_[e lew_l in _:he case of white>box rnonit.,,)rin_, ,_r ;tt the byte co_lc l_,v_l in t.he cas_, of black-box monit.oting. The idea of itsing t,emporal logic in progra.m testing is not, rmw. W_ ,rely m,'.nt.ion the commercial Tempor;_l F[ow:r tool (TR) [3] _'hich irr_plcrnents tempor;tl logics in a whit,e-b_x fgLshior_,and t,he MaC tool [13] whictt inlp[c_nl_:nts a special past time tmnporal logic in _tblacl<-box style. Er'ror pattezvz analy._',.._'consists of aalalyzing one execution _race using various error detection algorithms that can idcnt, ify error-prone programming practices, such as unhealthy locking disciplines that may lead to dat, a rnces and/or deadlocks. The important and appealing aspect of these algorithms is that they find error potentials even in the case where errors do not, explicit]y occur in the examined execution trace, but it is worth mentioning _,hat these algorithms are usually neither sound nor complete for the class of errors they are designed for. They are generally fast and scalable, and often catch the problems they are designed to catch, that is, the randomness in the choice of run does not seem to imply a similar randomness in the analysis results. Two such known algorithms focusing on concurrency errors have been implemented in JPAX, one for deadlocks and the other for data races, but the system is designed in such a way that users can relatively easily attach new such algorithms. The paper is organized as follows. Section 2 gives an overview of JPaX. Section 3 describes the underlying logic formalisms for writing requirement specifications, while Section 4 describes some of the error detection algorithms for debugging concurrent programs. Finally, Section 5 contains conclusions and a description of future work. 2 Overview of JPAX We next shortly describe JPAX's architecture. Unless otherwise specified, the black-box monitoring approach is considered. We use the acronym JP.a_Xx (Java PathExplorer Expander) when we refer to the white-box monitoring aspect of JPAX. White-box monitoring can be used in conjunction with black-box monitoring and works as follows: after one annotates the source code with desired formal requirements, one passes that source file through the white-box monitoring filter, JPAXx, and the annotations will be then expanded automatically into Java source code using optimal algorithms mentioned later in the paper, where after the expanded code may be compiled as normal and executed; exceptions will be thrown when formulae are violated. We next discuss the architecture of the black-box monitoring part of our system. JPAX can be regarded as consisting of three main modules: an instrumentation module, an observer module, and an interconnection mod- ule that ties the other two together through the observed event stream. The instrumentation module performs a script-driven automated instrumentation of the program to be observed. The instrumented program, when run, will emit relevant events to the inter-connection module, which further transmits them to the observation module. The observer may run on a different computer, in which case the events are transmitted over a socket. Hence, the input to JP._X consists of references to two entities: the Java program in byte code format to be monitored (created using a standard Java compiler) and the specification script defining the kinds of verification requested. The output is a (possibly empty) set of warnings printed on a special screen. More specifically, the specification script defines what (if any) kind of error pattern detection algorithms should be activated, and what (if any) kind of logic based monitoring should be performed, and in that case what the requirements are. For logic based monitoring, we have been inspired by the MaC language framework [13] and have split the specification into an instrumentation script and a verification script. The verification script identifies the high level requirement specifications that events are to be checked against. The propositions referred to in these specifications are abstract boolean flags, and do hence not refer directly to entities in the concrete program. The instrumentation script establishes this connection between the concrete boolean program predicates and the abstract propositions. The advantage of this layered approach, as also stated in [13], is that the requirement specification can be created without considering low level issues, and can even be created before the construction of the program. Currently, the scripts are written in Java. Thus, high level Java language constructs can be used to define the boolean predicates to be observed. The Java byte code instrumentation is performed using the powerful Jtrek Java byte code engineering tool [2J from Compaq. Jtrek makes it possible to easily read Java class files (byte code files), and traverse them as abstract syntax trees while examining their contents, and insert new code. The inserted code can access the contents of various runtime data structures, such as for example the call-time stack, and will, when eventually executed, emit events carrying this extracted information to the observer. Th('(_bs(u',_re:rc:r(qv(:_.s,h(_ w(,nts and <lispat.dtes t,hese _',_>a set of obs(_rv(:r rules, each rul(', pruforming a particular a.na.lysis t,har, has b(._m requested m the verification script. G_:n(_rally, t.his modular rule b_k_e<ldesign allows a user to easily define new runtitne verification procedures without interfering with legacy code. Observer rules are written in Java, but can call programs written in other languages, SUCh as [or example Maude. Maude plays _ special role in that hish level requirement specifications can be written in the Maude rewriting logic. The Maude rewriting engine cart then be used in two different ways: as a monitoring engine during program execution, or as a translation mgine before execution. In the former case, execution events are submitted to the Maude program, which in turn evaluates them against the requirement specification. In the latter case, the specification is translated into a data structure optimal for program monitoring, which is then sent back to Java, and used within the Java program to check the events during execution. ./PAX is built on a goner6: environment, named PathExplorer (PAX), which only consists of the inter- connection module and the observer module. The goal is to make it possible to monitor programs in other programming languages, such as for example C and C++, by just providing a language specific instrumentation module. Such an experiment has been performed in collaboration with Rich Washington, a member of the Robotics group at NASA Ames, on a 90,000 line C++ application for controlling a rover. The experiment just activated the deadlock detection rule, and located a deadlock potential in the application that had not been discovered through testing. 3 Logic Based Monitoring Logic based monitoring consist,; of checking execution events against a user-provided requirement specification written in some logic, typically an assertion logic with states as models, or a temporal logic with traces as models. JPAX allows the user to define such new logics in a flexible manner using the Maude algebraic specification language. Maude [1] is a modularized specification and verification system that very efficiently implements rewriting logic. JPAX currently provides linear temporal logics, both future time and past time, as builtin logics. Notice that multiple logi :s can be used in parallel, so each property can be expressed in its most suitable language. 3.1 Future Time LTL Semantics We first present a semantics o_"finite trace LTL using standard mathematical notation. Assume two total functions on traces, head : Trao_. _ Event returning the head event of a trace and length returning the length of a finite trace, and a partial flmction tail : Trace --_ Trace for taking the tall of a trace. That is, head(e, t) = head(e) = e, tail(e, t) = t, and ,ength(e) = 1 and length(e, t) = 1+ length(t). Assume further for any trace t, Chat t_ denotes the suffix trace ihat starts at position i, with positions starting at 1. The satisfaction relation C Trace × Formula defines wh,m a trace t satisfies a formula f, written t _ f, and is defined inductively over the structure of the formulae as :bllows, where Ais any atomic proposition and Xand Yare any formulae, and op are standard binary propositional connectives(v, and, -,, --_) and [], <>, (), U stand for always in the future, eventually in the future, next, ard until respectively: t _ ,t iff I E head(t) t _ ,.ruo iff true, t _ Ial!!ll iff false, t._ -_ X iff not t N I, t _ op '/ iff t _lop t_='t, t _ I]X iff (V i <_length(t)) tl _ X t _ ,>X iff (3 i < length(t)) tl _ X t _ 1 U r iff (_ i< length(t)) (ti _ Y and (V j <_ i) ti _ X) t _ I)X iff (if tail(t) is defined then tail(t) _---Xelse t _ X) Notice that liveness properties do not really make sense in finite trace LTL without statistical analysis, as already noticed in [12, 4]. In particular, the formula [] oa is violated if and only if a is false in the last observed state of the monitored program. The formula *(Oa V O",a) is always true in finite trace LTL and our optimal generator mentioned in subsection 3.3 proved that. 3.2 Past Time LTL Semantics Here w¢_pte_(:rlt the sermmti(:s of Hnir,c. trace p:_st thne t.empor_d [ogfi:. For prz._ttim(; t,he deHniti(>Hs ch_nge as f()Ilows: la._e(t, e) = la._t(e_) = c, front(t, e) = t, and length(e) = [ and length(t,e) = [ + length(t). Assume 5zrther for ztt_.y t,rztce t, that t_ denotes the prefix trace that ends at position i. The satisfact, ion relation C_ Trace × Formula defines when a trace t satisfies a formula f, writt, en t _ f, and is defined inductively over the structure of the formulae _ follows, where A is any atomic proposition and x and Yare any formulae, op are standard binary propositional connectives(v, and, -_, _), and [*], <*>, (*), S st_nd for always in the p_t, eventually in the past, previous, and since respectively: t _ a iff xElast(t) t _=:true iff true, t ,_ false iff ]alse, _ _ X iff not t _ X, t_x o_,r iff t_xopt_Y, t _ [.]X iff (V i <_length(t)) t_ _ X t _ <*>X iff (B i <_length(t)) tl _ X _ X S Y iff (3 i < length(t)) (tl _ Y and (V j < i) ti _ X) t _ (*)X iff (if front(t) is defined then front(t) _ Xelse t _ X) 3.3 Efficient Observer Generation After experimenting with runtime verification algorithms for LTL [10, 15, 11], each with its advantages and drawbacks, we realized that in order for one to properly compare these, one needs to first understand and establish criteria for "good" runtime verification algorithms. Consider a fixed logic. The following is are some priorities that we also discussed in [12] which currently influence the choice of runtime algorithms in JPAX : 1) for'wards design - algorithms that visit the execution traces backwards involve storing the trace and cannot throw exceptions or guide the program when a formula is violated, so we exclude them; 2) runtime efficiency - the normal execution of the program should be influenced as little as possible, so we exclude algorithms that are worse than linear in the size of the trace and prefer algorithms that are not exponential in the size of formula if possible; 3) initialization - the time required to generate code or data structures from formulae cannot be ignored, but it is considered less important than the previous criteria. Next we very briefly present some concepts that lead to a future time finite-trace LTL formula-checking algorithm that is the best one of which we are aware satisfying the criteria above. It visits the execution trace forwards and its worst-case runtime complexity is O(nk), where n is the length of the trace and k is the number of variables of the formula. The complete details together with optimality proofs will appear elsewhere soon. The interested reader can consult [12] for more detail. We have designed and implemented in Maude (in less than 200 lines of code) a relatively easy and elegant procedure that generates an optimal BTT finite trace FSM from any LTL formula. Despite its worst-case exponential complexity, it is quite fast on typical formulae: it needed more than 1second only on hand-crafted artificial formulae. This initialization time is spent only once, at the beginning of the monitoring. The following are a few examples of optimal BTT finite trace finite state machines generated by our current implementation: next end Formula I State _oa 1 1 a?true :false o(_aV O-_a) 1 1 true [](a -+ ob) 1 a?(b?l :2) : 1 a?(bTtrue :false) :true 2 b?l :2 b?true :false aL/ (bL/c) c?true :(a?l : (b?2 :false)) c?true :false c?true : (b?2 :false) c?true : false Notice that the generated finite state machines are deterministic. The drawback of generating deterministic machines is that they may be quite large for some formulae, even large enough that one cannot afford to generate and store them in practical situations. For that reason, we intend to also attach a module that generates nondeterministic automata from LTL formulae, like in [4], to JPAX to be activated when the deterministic one cannot be generated in a reasonable amount of time. 3.4 White-box Monit,)ring Theproceduraebove can be u_ed in instrumented bytecode monit, oring (black-box) _kswell as in source (:ode level monitoring (white-box). I_"t.he source code is available, the second approach may be more desired for two reasons: exception handling an, l efficiency. With regards to exceptions, white-box logic monitoring can now be seen as a natural extension to Ihe language _hat, allows one to describe conditions that should raise exception, as already noticed in [3]. As stated earlier, the worst-,:ase runtime complexity for future time LTL monitoring is O(nk), where n is _he length of the trace and k is the :mmber of variables of the formula. For the past time monitoring, the worst-case runtime complexity becomes O rim), where n is the same as above and m is the number of subformulae of the formula. We conjecture that th ._complexity of past time monitoring can be further improved• To demonstrate the tool we use a very simple example involving the monitoring of a traffic light controller The foilowing is an annotation 'left) and the expanded form of that annotation (right). <code> <code> /* JPaX: after green comes yello_ try { swizch(bztFsmState) { A_om isled = <boolean exp>; case I : Atom isGreen = <boolean exp>; bzzFsmS_ate = isGreen ? isYellow ? 1 : isRed ? 0 : 2 : I; break; A_om isYellow = <boolean exp>; case 2 : bt_FsmState = isYellow ? 1 : isRed ? 0 : 2; break; Formula : } []( isGreen -> ( ! isled U isYellow )); if(bttFsmStaZe == O) throw new ExcepZion("Prop. Failure"); ./ } ca:oh(Exception e) { Syszem,out.prin_in(e.getHessage()); } <code> <code> The annotation is commente t out in a normal Java comment but contains the keyword JPaX followed by a title, a list of atomic declaratior s, and an LTL formula. Here the formula states "it is always the case that if the light is green it will not be ied again until it has first been yellow"• Now this new code may be compiled normally and will raise an exception if the property is violated. Next we look at the same e.,ample, but now we express the property in past time finite trace LTL. Here we took the dynamic programming algorithm for future time LTL presented in [15] and converted it to past time LTL. We are planning a feIlow up paper that will discuss these algorithms in more detail. Once again the annotation is on the left an t the expanded annotation is on the right. Not seen in this example is the initialization of the array prey, which holds the evaluation of a particular subformula in the previous state. Here the formula states "if the light is red then the light has not been green since it was yellow" <code> <code> /* JPaX: after green comes yellow now[6] = isGreen; now[S] = isYellow; Atom isRed = <boolean exp>; now[4] = ! now[6]; Atom isGreen = <boolean exp>; now[3] = now[5] Jl (now[4] && prey[3]); Atom isYellow = <boolean exp>; now[2] = isRed; now[l] = ! now[2] If now[3]; Formula : prev[3] -- now[3] ; isRed -> ( ! isGreen S isYeilow); if (! prey Ill) { throw new Exception("Prop. Failure");} -/ <code> <code> The ordering of the above statements is the result of parsing the formula and then visiting each subformula in the parse tree in a breadth first ordering from the bottom up. When the expanded code is executed, each statement is evaluated to determi;te whether the subformula holds in that state or not. 4 Error Pattern Analysis Error pnt,Umn runtime analysis algorithms explore an execution trace and detect error potentials. Tile important and ;q)pealing aspect of these algorithms is that. they find error potentials even in the case wh_:re errors do not explicitly occur in the examined execution trace. They are usually fast and scalable, and often catch the problems t,hey are designed to cat,ch, that is, the randomness in the choice of run does not seem to imply a similar randomness in the analysis results. The trade off is _hat they have less coverage than heavyweight formal methods and often suggest problems which, after a careful semantical analysis, turn out not to be errors. Two examples of such algorithms focusing on concurrency errors have been implemented in .IPAX: the Eraser [16J data race analysis algorithm and a deadlock analysis algorithm based on analyzing lock cycles. Both these algorithms have been previously implemented by Compaq in the Visual Threads tool [6] to work for C and C++. 4.1 Data Race Analysis We briefly describe here how easily data races can occur in concurrent programming and how Eraser [16] has been implemented in JPAX to work on Java programs. A data race occurs when two or more concurrent threads access a shared variable, at least one access is a write, and the threads use no explicit mechanism to prevent the accesses from being simultaneous. The Eraser algorithm detects data races by studying a single execution trace of the monitored program, trying to conclude whether there exist valid runs where data races are possible. We illustrate the data race analysis with the following example. 1. class Value{ 2. private int x = 1; 3. 4. public synchronized void add(Value v){x = x + v.getO;} 5. 6. public int get(){return x;} 7.} 8. 9. class Task ex_ends Thread{ 10. Value vl; Value v2; 11. 12. public Task(Value v1,Value v2){ 13. this.v1 = vl; _his.v2 = v2; 14. _his.s_ar_(); is. } 16. 17. public void run(){vl.add(v2);} Is.} 19. 20. class Main{ 21. public static void main(String[] args){ 22. Value vl = new Value(); Value v2 = new Value(); 23. new Task(vl,v2); new Task(v2,vl); 24. } 25.} The classValue containsan integervariablex,asynchronizedmethod add thatupdatesx by adding thecontent ofanother Value variable,and an unsynchronizedmethod get thatsimply returnsthevalueofx. Task isa threadclass:itsinstancesarestartedwith themethod start which executestheuserdefinedmethod run. Two such tasksarestartedinMain,on two instancesoftheValue class,vl and v2. When running JPAX with the Eraseroptionswitchedon,a dataracepotentialisfound,reportingthatthevariablex inclassValue isaccessed unprotected by thetwo threadsinlines4 and 6,respectivelyT.he generatedwarning message givesa scenario under which a data racemight appear,summarizing the following.One Task threadcan callthe add method on the objectvl with the parameter Value objectv2,whose contentisthus readviatheunsynchronized get method. The otherthreadcansimultaneouslydo thedualthing,i.e.c,alltheadd method on v2.Therefore,the contentofv2 might be accessedsimultaneouslyby thetwo threads. Roughly, thealgorithmworks and isimplemented inJPAX asfollows.The instrumentedbyte code ofthe monitored program emits to the observer appropriate events when variables are read or updated, and when locks are acquired or released as a result of executing Java's synchronized statements or from calling/returning from synchronized methods. The observer maintains two data structures: a thread map that keeps track of all the locks owned by _';L,:i_t.hreal[, ;u d ;t mLmahl,_ map that, a._s_3ciat,es with each (:shared) variable th, intersection of the Sl_t, O[ [¢3(:ksthat h;l."; t)e_ll :_)mnitmly owned by all accessing threads in r,he past. If this set ever becomes empty then a data race potential exists. More precisely, when a variable is accessed for the first time, ghe locks ownecl by the accessirig thread _t,that monmnt arestored in the variable',_ variable set. Subsequent accesses by other t,hre;uts causes t,he set t,o be re/-ined to its intersection with r,he locks owned by those t,hreads. An extra st,ate machine is also rnaintaine, t for each variable I',okeep track of how many r,hreads have accessed the variable and how (read/write). This is _sed t,oreduce the number of false warnings, such as situations in which variables are initialized by a single thread without locks (which is safe) or several t,hreads only read a variable after it has been initialized (which is also safe). Deadlock Detection Deadlock potentials are hard to find in general, but there are classical deadlock situations which occur when multiple threads take locks in d fferent order. For example, a deadlock will arise if a thread acquires a lock and then, without releasing it, acquires another lock, while another thread first acquires the second lock and then the first one. One can simply create such a situation in the previous Java example if one wrongly tries to repair the data race by also defining the get method in line 6 as synchronized: 6. public synchronized int g_t(){return I;} It is clear now that the data ra:e algorithm wilt indeed not return a warning anymore because the variable x can no longer be accessed simultaneously from two threads. However, there is a deadlock potential now and JPAX detects it. More exactly, when running JPAX on the modified program, a lock order problem is found and an appropriate warning message is issued summarizing the fact that two object instances of the Value class are taken in a different order by the two Task threads. It also indicates the line numbers where the threads may potentially deadlock: line 4 where the get method called from add may lock the second object. Notice that this deadlock doesn't need :o appear in the examined trace in order for this warning to be issued. In fact, deadlock potentials might be reported in general even if those deadlocks will never appear in any execution of the program. Any execution of the modified program above will cause a warning to be issued. The runtime deadlock analysis algorithm is also implemented in the observer and it needs only a subset of the events generated for the data race algorithm, namely those related to acquires and releases of locks that result from executing Java's syr chronized statements or from calling/returning from synchronized methods. Two data structures are maintalaed in the observer: as in the data race algorithm a thread map keeps track of the locks owned by each thread, while a second data structure, a lock graph, updates a graph that accumulates as nodes all the locks taken by any _hread during an execution, the edges recording locking orders. In other words, an edge is introduced from a loci: to another each time when a thread that already owns the first lock acquires the other. If during the executio_t of the program this graph becomes cyclic, then there is a deadlock potential related to lock ordering in the program. This simple algorithm can reveal more complex deadlock potentials between more than two threads, as illustrated for example by the classical dining philosopher's example. 5 Conclusions We have presented JPAX, a ruT time verification tool under development at NASA Ames Research Center. JPAX provides an integrated environment for instrumenting Java byte code to emit events during execution to an observer, which performs two kinds of analysis: logic based monitoring, checking events against high level requirements specifications, and error pattern analysis, searching for low level programming errors. It has been shown how the two kinds of verif cation can be combined by viewing them as rules within an extensible set of rules. A white-box logic based monitoring approach has also been presented. In the case where efficiency is required, we have shown that optimal data structures can be generated from future time and past time LTL. Finally, two known error pattern detection algorithms, one for data races and one for deadlocks, have been implemented to work on Java. Of other future work can be mentioned that we will experiment with new logics in Maude more appropriate to monitoring than LTL, such as interval and real time logics and UML notations. Future work on error pattern analysis will try to develop new algorithms for detecting concurrency errors other than data races and deadlocks, and of course to try to improve e_isting algorithms. We will also stud) completely new functionalities of the system, such as guided execution via code instrumentation to explore more of the possible interleavings of a mm-,h,t(wrnh_isti(: <(recurrent l)togra, m dltt'ing _,estin,K. Dv).rmic progra.m visualizar, iou _ al_(> , fi_(',ur(_ s_tb.ject, whet(, w_ regard a visualizat, i(m pa(:l_tg(._ ;us just, anoth(_r t'uh' in the observer. A more user" [riendlv int,erface, both graphical and functional, will be provide.d, and ['innllv t,he t,ool will be evaluated against NASA safety crit, ical applications. References [11 M. Clavel, F..l. Durgn. S. Eker, P. Lincoln, N. Martf-Oliet, .I. Meseguer, and J. F. Quesada. The Maude System In Proceedings of the lOth fnternational Conference on Rewriting T,_chniques and Application_ (RTA-g9)_ volume 1631 of LNCS, pages 240-243, Trento, Italy, July 1999. Springer-Verlag. System description. [2] S. Cohen..Itrek. Compaq, ht_:p ://wv_. compaq, com/j ava/download/j'crek. [3] D. Drusinsky. The Temporal Rover and the ATG Rover. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 323-330. Springer, 2000. [4] Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata. In Proceedings of the First International Workshop on Runtime Verification, volume 55(2) of Electronic Notes in Theoretical Computer Science. Elsevier, 2001. [5] B. Fischer, T. Pressburger, G. Rosu, and J. Schumann. The AutoBayes Program Synthesis System - System Description. In Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2001), Siena, Italy, June 2001. [6] J. Harrow. Runtime Checking of Multithreaded Applications with Visual Threads. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 331-342. Springer, 2000. [7] K. Havelund. Using Runtime Analysis to Guide Model Checking of Java Programs. In SPIN Model Checking and Software Verification, volume 1885 of LNCS, pages 245-264. Springer, 2000. [8] K. Havelund, M. Lowry, and J. Penix. Formal Analysis of a Space Craft Controller using SPIN. In Proceedings of the gth SPIN workshop, Paris, barance, November 1998. To appear in IEEE Transactions of Software Engineering. [9] K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4):366-381, April 2000. Special issue of STTT containing selected submissions to the 4th SPIN workshop, Paris, France, 1998. [lOJ K. Havelund and G. Ro§u. Testing Linear Temporal Logic Formulae on Finite Execution Traces. RIACS Technical report, ht'cp ://ase. arc. nasa. gov/pax, November 2000. [11] K. Havelund and G. Ro§u. Java PathExplorer - A Runtime Verification Tool. In Proceedings of the 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS'01), Montreal, Canaxta, June 2001. [12] Klaus Havelund and Grigore Ro§u. Monitoring Java Programs with Java PathExplorer. In Proceedings of the First International Workshop on Runtime Verification, volume 55(2) of Electronic Notes in Theoretical Computer Science. Elsevier, 2001. [13] I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan. Runtime Assurance Based on Formal Specifications. In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999. [14] M. Lowry, A. Philpot, T. Pressburger, I. Underwood, R. Waldinger, and M. Stickel. Amphion: Automatic Pro- gramming for the NAIF Toolkit. In NASA Science Information Systems Newsletter, volume 31, February 1994. [15] G. Ro§u and K. Havelund. Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae. RIACS Technical report, http://ase.arc.nasa.gov/pax, Januaxy 2001. [161 S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems, 15(4):391-411, November 1997. [171 W. Visser, K. Havelund, G. Brat, and S. Park. Model Checking Programs. In Proceedings of ASE'2000: The 15th IEEE International Conference on Automated Software Engineering. IEEE CS Press, September 2000. [181 J. Whittle and J. Schumann. Generating Statechart Designs From Scenarios. In International Conference on Software Engineering (ICSE 2000), Limerick, Ireland. June 2000.