|
|
|
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 Download: here
- 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
|
|
