USC Center for Software Engineering Presents
Los Angeles
Software
Process Improvement Network
Wednesday, Dec. 1, 5:30 P.M.
to 8:30 P.M.
"Formal
Methods Used in for Practical
Software Verification"
Speaker: Robert T. Bauer,
IBM
In the
formal methods
community, software verification means to prove that a given software
system is
correct with respect to its specification.
Engineers and managers in software Quality Assurance (QA) and
Quality
Engineering (QE) have a different problem:
Increasingly complex software that needs to be "tested" in
ever decreasing amounts of time.
Even if you prove that some software system is correct (with
respect to
its specification), you still need to test the software system. This does not mean that the techniques of
formal
methods are "orthogonal" with those used by QA/QE teams.
It means that QA/QE teams will be more
effective if they understand the ideas and limitations of formal
methods. QA/QE teams can incorporate many
of the
concepts and even the techniques themselves within the test environment.
While many
practices of
formal methods are quite mathematical and complicated, the techniques
themselves are quite simple. This talk
gives a high-level overview of these techniques and shows how they
apply at a
very practical level to the problems faced by QA/QE teams.
Robert
T. Bauer has over 15 years
of
industry experience. He has worked in
research labs and in real-world business application development. At Quantum Dynamics' Advanced Experimental
Research Laboratory, Robert developed the real-time kernel for NASA's
Cryogenic
Orbital Depot Satellite. At PDS, he
developed inventory, order processing, shipping and customer service
applications to support a full-service fulfillment center.
At 1776, Robert developed fault-tolerant
disk array software and at NCR, he developed a wide-variety of software
to
support large-scale testing of the Teradata database.
His Parallel Test Environment (PTE) is now the standard testing
environment at NCR and is used at the 5 Teradata development centers. He began working in formal methods at NCR
and continued that work at Levetate where he worked on the semantics of
a
behavioral specification language and developed a theorem prover for
automated
formal verification. Robert is now with
IBM where he spends most of his time working on design pattern software
and on
formal methods related work.
Robert is
well-known in the
software quality community for his contributions to software testing. Robert developed a testing strategy called
Customer-Based Testing. This strategy
combines software reliability engineering, automatic test case
generation, and
usage coverage to minimize the risk of expensive failures and maximize
assurance of base functionality. Robert
introduced Early Regression Testing. At
NCR, early regression testing moved 70% of the problems discovered at
system
test to feature/unit testing. Robert
has undergraduate degrees in Electrical and Industrial Engineering and
a
graduate degree in Computer Science.
***
Recheck the web site before
the meeting ***
Location: University of
Southern California - Information Sciences Institute
11th
Floor
Conference Room, 4676 Admiralty Way, Marina Del Rey, CA
90292-6601
Map
and directions at http://sunset.usc.edu/cse/pub/event/LASpin.html
| Directions
|
5:30
to 6:00 Networking |
7:00
to 7:30 Networking |
|
6:00
to 7:00 Presentation |
7:30
to 8:30 Presentation cont’d |
No reservations needed. Free parking in nearby structure, bring ticket to meeting for validation.
For additional information: http://sunset.usc.edu/cse/pub/event/future/index.html or LASPIN2004@yahoo.com