Skip past navigation stuff NASA Langley Formal Methods



quick page







Welcome to the NASA LaRC/NIA Formal Methods
Coffee Colloquium Series
The NASA LaRC/NIA Formal Methods Coffee Colloquium Series is scheduled to occur on Fridays at 10:30am, on a biweekly basis.  No colloquium will occur when a NIA Formal Methods Seminar is being held.  The Coffee Colloquium will be held at NASA LaRC, Bldg 1220, Room 110.  NIA Formal Methods Seminars are held at the National Institute of Aerospace, Room 404.

If you would like give a talk at the Coffee Colloquium Series, please contact Lee Pike at or +1 757-864-6193.  The NIA Formal Methods Seminars are organized by César Muñoz.

We are happy to invite anyone who is interested to attend the Coffee Colloquium Series.  Please note the following two caveats, however: (1) Presentations at the Coffee Colloquia are often very informal, and (2) If you do not have access to NASA Langley, you will need to obtain an invitation from a NASA LaRC civil servant in advance of the colloquium.  NIA Formal Methods Seminars are open to the general public, and all are invited to attend.

Upcoming Talks

  • Friday, April 15st 10:30am (Catering: Lee Pike)
    • Title: Real Number Calculations and Theorem Proving
    • Abstract: Wouldn't it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this talk we outline how this can be done in PVS. First, we formally establish upper and lower bounds for trigonometric and transcendental functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations can be performed in an algebraic setting. This pragmatic approach has been implemented as a PVS strategy. The strategy provides a safe way to perform explicit calculations over real numbers in formal proofs.
    • Paper & PVS Specifications Downloadhere
    • Slides Download: pdf
  • Friday, April 29th 10:30am (Catering: César Muñoz)
    • Speaker: Lee Pike
    • Title: How (NOT!) to Axiomatize Time-Triggered Systems
    • Abstract: I describe a well-cited axiomatization of time-triggered systems that appears in the IEEE Transactions on Software Engineering and specified and verified in PVS.  I describe the use of PVS's theory interpretations to show that a canonical model  does not satisfy the three of the four axioms presented, and in fact, that they are unsatisfiable.  I provide simple repairs for axioms.  Finally, I describe ongoing work to show using SAL that the scheduling characteristics of a prototype of the ROBUS satisfies constraints derived from the repaired axioms.

  • Friday, May 13th: No colloquium (NIA Formal Methods Seminar)
  • Friday, June 3rd 10:30am (Catering: Radu Siminiceanu)
    • Speaker: Paul Miner (reporting joint work with Alfons Geser)
    • Title: A set of generic PVS theories for verifying a class of synchronization protocols.
    • Abstract: In this talk, I will summarize recent work to provide a generic
      verification framework for periodic discrete-update clock synchronization protocols.  The PVS theories provide reusable, protocol-independent, proofs of the top-level clock synchronization properties of precision and accuracy.   The accuracy results are sufficiently flexible to allow for proofs of optimal accuracy, as defined by Srikanth & Toueg.   The proofs follow from a collection of invariant properties that we expect to hold for periodic, discrete-update protocols.  The general theory is illustrated with two representative instances.  The first is the Welch & Lynch protocol employed by TTP/C.  The other is the SPIDER protocol, which was adapted from Srikanth & Toueg.
  • Friday, June 17th 10:30am (Catering: Paul Miner)
    • Speaker: Songtao Xia
    • Title: Toward Automated Test Generation for Engineering Applications via Predicate Abstraction
    • Abstract: In test generation based on model-checking, white-box test criteria are represented as trap conditions written in a temporal logic. A model checker is used to refute trap conditions with counter-examples. From a feasible counter-example test inputs are then generated. Earlier research has demonstrated the usefulness of this approach and revealed its weaknesses.  The major problems of applying this approach to engineering applications derive from the fact that engineering programs have an infinite state space and non-linear numerical computations. Our solution is to combine predicate abstraction (which reduces the state space) with a numerical decision procedure (which supports predicate abstraction by solving non-linear constraints) based on interval analysis.  We have developed a prototype and applied it to MC/DC (Modified Condition/Decision Coverage) test case generation. We have used the prototype on a number of C modules taken from a conflict detection and avoidance system and from a Boeing 737 autopilot simulator. The modules range from tens of lines up to
      thousands of lines in size. Our experience shows that although in theory
      the inclusion of a decision procedure for non-linear arithmetic may lead
      to non-terminating behavior and false positives (as abstraction-based
      model checking already does), our prototype is able to automatically
      produce feasible counterexamples with only a few exceptions. Furthermore, the process runs with acceptable execution times, without requiring any other knowledge of the specification, and without tampering with the original C programs.
  • Friday, July 1st 10:30am (Catering: Songtao Xia)
    • Speaker: Radu Siminiceanu
    • Title: TBA (on saturation in SAL/variable ordering in SMART/self-stabilization protocol verification in SMART)
    • Abstract: TBA

  Skip past bottom navigation 
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Lee Pike
larc privacy statement
last modified: March 2005

Bobby Approved