Formal specification languages have long languished, due to the grave scalability problems faced by complete verification methods. Runtime verification promises to use formal specifications to automate part of the more scalable art of testing, but has not been widely applied to real systems, and often falters due to the cost and complexity of instrumentation for online monitoring. In this paper we discuss work in progress to apply an event-based specification system to the logging mechanism of the Mars Science Laboratory mission at JPL. By focusing on log analysis, we exploit the "instrumentation" already implemented and required for communicating with the spacecraft. We argue that this work both shows a practical method for using formal specifications in testing and opens interesting research avenues, including a challenging specification learning problem.

Runtime verification as a field faces several challenges. One key challenge is how to keep the overheads associated with its application low. This is especially important in real-time critical embedded applications, where memory and CPU resources are limited. Another challenge is that of devising expressive and yet user-friendly specification languages that can attract software engineers. In this paper, it is shown that for many systems, in-place logging provides a satisfactory basis for postmortem “runtime” verification of logs, where the overhead is already included in system design. Although this approach prevents an online reaction to detected errors, possible with traditional runtime verification, it provides a powerful tool for test automation and debugging—in this case, analysis of spacecraft telemetry by ground operations teams at NASA’s Jet Propulsion Laboratory. The second challenge is addressed in the presented work through a temporal specification language, designed in collaboration with Jet Propulsion Laboratory test engineers. The specification language allows for descriptions of relationships between data-rich events (records) common in logs, and is translated into a form of automata supporting data-parameterized states. The automaton language is inspired by the rule-based language of the RULER runtime verification system.A case study is presented illustrating the use of our LOGSCOPE tool by software test engineers for the 2011 Mars Science Laboratory mission.

This paper describes the evolution of a software testing effort during a critical period for the flagship Mars Science Laboratory rover project at the Jet Propulsion Laboratory. Formal specification for post-run analysis of log files, using a domain-specific language, LogScope, replaced scripted real-time analysis. Log analysis addresses the key problems of on-the-fly approaches and cleanly separates specification and execution. Mining the test repository suggested the inadequacy of the scripted approach, and encouraged a partly engineer-driven development. LogScope development should hold insights for others facing the tight deadlines and reactionary nature of testing for critical projects. LogScope received a JPL Mariner Award for "improving productivity and quality of the MSL Flight Software" and has been discussed as an approach for other flight missions. We note LogScope features that most contributed to ease of adoption and effectiveness. LogScope is general and can be applied to any software producing logs.

Automated planning systems (APS) are maturing to the point that they have been used in experimental mode on both the NASA Deep Space 1 spacecraft and the NASA Earth Orbiter 1 satellite. One challenge is to improve the test coverage of APS to ensure that no unsafe plans can be generated. Unsafe plans can cause wasted resources or damage to hardware. Model checkers can be used to increase test coverage for large complex distributed systems and to prove the absence of certain types of errors. In this work we have built a generalized tool to convert the input models of an APS to Promela , the modeling language of the Spin model checker. We demonstrate on a mission sized APS input model, that we with Spin can explore a large part of the space of possible plans and verify with high probability the absence of unsafe plans.

NASA spends millions designing and building spacecraft for its missions. The dependence on software is growing as spacecraft become more complex. With the increasing dependence on software comes the risk that bugs can lead to the loss of a mission. At NASApsilas Jet Propulsion Laboratory new tools are being developed to address this problem. Logic model checking and runtime verification can increase the confidence in a design or an implementation. A barrier to the application of such property-based checks is the difficulty in mastering the requirements notations that are currently available. For these techniques to be easily usable, a simple but expressive requirement specification method is essential. This paper describes a requirements capture notation and supporting tool that graphically captures formal requirements and converts them into automata that can be used in model checking and for runtime verification.

In this study, we developed three optimized peptide ligands (OPL) that demonstrate increased affinities for HLA-A*0201 compared with wild-type tyrosinase-related protein-2 (TRP-2) peptide. The OPL contain amino acids from TRP-2(180-188) and preferred primary and auxiliary HLA-A*0201 anchor residues. Cytotoxic T lymphocyte (CTL) lines were generated against wild-type TRP-2 peptide and OPL by multiple rounds of peptide stimulation of peripheral blood mononuclear cells from HLA-A2*0201+ healthy individuals. CTL reactivity profiles to three different OPL were donor-dependent. Among donors, at least one OPL was particularly stimulatory and elicited high levels of CTL that cross-reacted with wild-type TRP-2 peptide. Cytotoxicity assays using CTL raised on wild-type TRP-2 peptide or OPL demonstrated lysis of HLA-A2-positive glioblastoma cells. Molecular models of TRP-2 and OPL peptides docked with HLA-A*0201 demonstrated that substitution of F for S at position 1 (P1) oriented the peptides favoring a pi–pi aromatic interaction with W 167 of HLA-A*0201. This in turn positions P5 and P8 aromatic rings to face solvent that may promote binding to the T-cell receptor, leading to a robust T-cell activation. The results of this study further substantiate the concept that rational design and testing of multiple peptides for the same T-cell epitope should elicit a broader response among different individuals than single peptide immunization. Our results may partially explain why some patients have better clinical responses to peptide-based immunotherapy, whereas others respond poorly.

Abstract- Automated planning systems (APS) are gaining,Expressing the Property of Interest .................... 6 acceptance for use on NASA missions as evidenced by APS($, ............................................................. spicecraft executes. The system mustbe verified to ensure BIOGRAPHY,10

Automated planning systems (APS) are gaining acceptance for use on NASA missions as evidenced by APS flown on missions such as Earth Orbiter 1 and Deep Space 1, both of which were commanded by onboard planning systems. The planning system takes high level goals and expands them onboard into a detailed plan of action that the spacecraft executes. The system must be verified to ensure that the automatically generated plans achieve the goals as expected and do not generate actions that would harm the spacecraft or mission. These systems are typically tested using empirical methods. Formal methods, such as model checking, offer exhaustive or measurable test coverage which leads to much greater confidence in correctness. This paper describes a formal method based on the SPIN model checker. This method guarantees that possible plans meet certain desirable properties. We express the input model in Promela, the language of SPIN (Holzmann, 1997 and Holzmann, 2003) and express the properties of desirable plans formally. The Promela model is then checked by SPIN to see if it contains violations of the properties, which are reported as errors. We have applied this approach to an APS and found a defect

This viewgraph presentation reviews work on model checking, and specifically the SPIN model checker. The goal of this work is to retire a significant class of risks associated with the use of Artificial Intelligence (Al) Planners on Missions. This effort must provide tangible testing results to a mission using Al technology. It is hoped that the work should be possible to leverage the technique and tools throughout NASA

In this study, we developed two Her-2/neu-derived E75 altered peptide ligands (APLs) that demonstrate increased affinities for the HLA-A*0201 allele compared with wild-type E75 peptide. The APLs contain amino acids from E75(369–377), an immunodominant Her-2/neu-derived peptide, and preferred primary and auxiliary HLA-A*0201 molecule anchor residues previously identified from combinatorial peptide library screening with the recombinant molecule. CTL lines were generated against wild-type E75 peptide (KIFGSLAFL) and APLs by multiple rounds of peptide stimulation of peripheral blood mononuclear cells (PBMCs) from HLA-A2+ antigen normal individuals. CTL lines raised on wild-type E75 peptide cross-reacted with APLs and similarly, CTL lines raised on APLs cross-reacted with wild-type E75 peptide, as measured by IFN-γ ELISpot and target cell lysis assays. One of five individuals demonstrated specificity for APL 2 (FLFGSLAFL), whereas APL 5 (FLFESLAFL)-specific responses were observed from all five individuals tested. Molecular models of the E75, APL 2, and APL 5/HLA-A2 complexes indicated that the substitution of glycine with glutamic acid at position four of APL 5 resulted in the presentation of a large, negatively charged side chain that interacts with the outer edge of the HLA-A2 antigen alpha helix and is freely available to interact with cognate T-cell receptors. The results of this study further substantiate the concept that rational design of T-cell epitopes may lead to stronger peptide immunogens than natural, wild-type peptides.

Unlike HLA-A and HLA-B, few peptide epitope motifs have been reported for HLA-C molecules. However, a number of cytotoxic T-lymphocyte epitopes derived from tumor antigens that bind to HLA-C molecules have been described. Here we report peptide-binding motifs for both HLA-Cw6.02 and HLA-Cw7.01 molecules. Recombinant human HLA molecules were generated and used to screen combinatorial 9mer peptide libraries. Complexes of HLA molecules properly folded and associated with β2-microglobulin and peptides were identified using a conformation-specific HLA class I antibody conjugated to alkaline phosphatase. In the presence of substrate, peptide beads can be readily isolated and microsequenced to determine peptide identity. Of the peptides that bound to HLA-Cw6.02 and HLA-Cw7.01, 19 and 18 peptides, respectively, were sequenced, allowing motif identification for each C allele. This is the first report of an HLA-Cw7.01 peptide motif and extends the findings of Falk et al. [(1993) Proc Natl Acad Sci USA 90:12005] for an HLA-Cw6.02 motif. Anchoring amino acids for the HLA-Cw6.02 motif were phenylalanine or tyrosine in position (P)1, arginine in P2, and an aliphatic/aromatic residue at P9. Anchoring residues for HLA-Cw7.01 were positively charged amino acids in P1 and P2. Unlike most other HLA molecules, we were unable to assign P9 an anchoring residue, and we suspect that HLA-Cw7.01 binds peptides in an unconventional manner. Additionally, preferred amino acids were identified for both molecules. Identification of HLA-Cw6.02 and HLA-Cw7.01 peptide-binding motifs makes a significant contribution to the C allele peptide-binding motifs and will allow investigators to predict, design, and test HLA-Cw6.02 and HLA-Cw7.01 engineered peptides for immunotherapy.

In this study, four modified gp100 peptides were designed by combining amino acids from the melanoma peptide antigen gp100((209-217)) with preferred primary and auxiliary HLA-A *0201 anchor residues previously identified from combinatorial peptide library screening with recombinant HLA-A*0201. These modified peptides demonstrated stronger binding affinity for the HLA-A*0201 molecule compared to wild-type gp100 peptide. Nine CTL lines generated from patients immunized with the g209-2 M peptide and one CTL line from a non-immunized patient were tested for the ability to respond to these modified gp100 peptides. Stimulation of CTL by two of four modified peptides induced higher levels of IFN-gamma secretion than the wild-type gp100 peptide, demonstrating that higher peptide binding affinity for HLA molecules does not necessarily equate to functional activity of CTL. Two major and one minor CTL recognition pattern were observed, irrespective of previous peptide immunization, suggesting that multiple, rationally designed modified tumor peptides for the same epitope stimulate a broad CTL response by activating multiple CTL capable of cross-reacting with the natural antigenic peptide.

Over the years, the complexity of space missions has dramatically increased with more of the critical aspects of a spacecraft's design being implemented in software. With the added functionality and performance required by the software to meet system requirements, the robustness of the software must be upheld. Traditional software validation methods of simulation and testing are being stretched to adequately cover the needs of software development in this growing environment. It is becoming increasingly difficult to establish traditional software validation practices that confidently confirm the robustness of the design in balance with cost and schedule needs of the project. As a result, model checking is emerging as a powerful validation technique for mission critical software. Model checking conducts an exhaustive exploration of all possible behaviors of a software system design and as such can be used to detect defects in designs that are typically difficult to discover with conventional testing approaches.

CD8+ T-lymphocytes recognize peptides in the context of major histocompatibility complex (MHC) class I antigens. Upon activation, these cells differentiate into effector cytotoxic T lymphocytes (CTL) and no longer require formal antigen presentation by professional antigen presenting cells (APC). Subsequently, any cell expressing MHC class I/cognate peptide can stimulate CTL. Using TIL specific for a melanoma antigen-derived peptide, IMDQVPFSV (g209 2M), we sought to determine whether these CTL could present peptide to each other. Our findings demonstrate that peptide presentation of the g209 2M peptide epitope by TIL is comparable to conventional methods of using T2 cells as APC. We report here that CTL are capable of self-presentation of antigenic peptide to neighboring CTL resulting in IFN-γ secretion, proliferation, and lysis of peptide-loaded CTL. These results demonstrate that human TIL possess both APC functions as well as cytotoxic functions and that this phenomenon could influence CTL activity elicited by immunotherapy.

Abstract: A logic model checker can be an effective tool for debugging software applications. A stumbling block can be that model checking tools expect the user to supply a formal statement of the correctness requirements to be checked in temporal logic. Expressing non-trivial requirements in logic, however, can be challenging. To address this problem, we developed a graphical tool, the TimeLine Editor, that simplifies the formalization of certain kinds of requirements. A series of events and required system responses are placed on a timeline. The user converts the timeline specification automatically into a test automaton, that can be used directly by a logic model checker, or for traditional test-sequence generation. We have used the TimeLine Editor to verify the call processing code for Lucent's PathStar Access Server against the TelCordia LSSGR standards. The TimeLine editor simplified the task of converting a large body of English prose requirements into formal, yet readable, logic requirements.

To formally verify a large software application, the standard method is to invest a considerable amount of time and expertise into the manual construction of an abstract model, which is then analysed for its properties by either a mechanized or a human prover. There are two problems with this approach. The first problem is that this verification method can be no more reliable than the humans that perform the manual steps. If the average rate of error for human work is a function of the problem size, this holds not only for the construction of the original application, but also for the construction of the model. The standard verification trajectory therefore tends to become less reliable for larger applications. The second problem is one of timing and relevance. Software applications built by teams of programmers can change rapidly, often daily. Manually constructing an accurate abstraction of any one version of the application, though, can take weeks, which may jeopardize the validity of the results. In this paper a different verification method that avoids these problems is discussed. This method, which may be the precursor of a new class of testing techniques, was originally developed to allow for a thorough testing of parts of the software of a new commercial telephone switch. Here it is argued, though, that the method also has broad applicability to distributed software systems design in general.

A significant part of the call processing software for Lucent's new PathStar™ Access Server was checked with formal verification techniques. The verification system we built for this purpose, named FeaVer, is accessed via a standard Web browser. The system maintains a database of feature requirements, together with the results of the most recently performed verifications. Via the browser the user can invoke new verification runs, which are performed in the background with the help of a logic model checking tool. Requirement violations are reported either as high-level message sequence charts or as detailed execution traces of the system source. A main strength of the system is its capability to detect potential feature interaction problems at an early stage of systems design. This type of problem is difficult to detect with traditional testing techniques. Error reports are typically generated by the system within minutes after a comprehensive check is initiated, allowing near-interactive probing of feature requirements and quick confirmation (or rejection) of the validity of tentative software fixes.

Formal verification methods are used only sparingly in software development. The most successful methods to date are based on the use of model checking tools. To use such tools, the user must first define a faithful abstraction of the application (the model), specify how the application interacts with its environment, and then formulate the properties that it should satisfy. Each step in this process can become an obstacle. To complete the verification process successfully often requires specialized knowledge of verification techniques and a considerable investment of time. In this paper we describe a verification method that requires little or no specialized knowledge in model construction. It allows us to extract models mechanically from the source of software applications, securing accuracy. Interface definitions and property specifications have meaningful defaults that can be adjusted when the checking process becomes more refined. All checks can be executed mechanically, even when the application itself continues to evolve. Compared to conventional software testing, the thoroughness of a check of this type is unprecedented.

ABSTRACT A significant part of the call processing,software for Lucent’s new,PathStar ™ access server [FSW98] waschecked,with automated,formal verification techniques. The verification systemwe built for this purpose, named FeaVer, maintains a database of feature requirements which is accessible via a web browser. Via the browser the user can invoke verification runs. The verifications are performed by the system with the help of a standard logic model checker that runs in the background, invisibly to the user. Requirement violations are reported as C execution,traces and stored in the database for user perusal and correction. The main,strength of the system is in the detection of undesired feature interactions at an early stage of systems design, the type of problem that is notoriously difficult to detect with traditional testing techniques. Error reports are typically generated by the system within minutes after a check is initiated, quickly enough to allow near interactive probing of requirements or experimenting with software fixes.