Systems Integrity, Software
Safety, and Process Security
June 27 - July 1, 1994
National Institute of Standards and Technology
Gaithersburg, MD
COMPASS Sponsors IEEE Aerospace and Electronics Systems Society
IEEE National Capital Area Council
In Cooperation With British Computer Society
Conference Sponsors Arca Systems, Inc.
ARINC Research Corporation
Control Systems Analysis, Inc.
CTA, Inc.
Logicon, Inc.
National Institute of Standards and Technology
Naval Research Laboratory
Naval Surface Warfare Center
Systems Safety Society
TRW Systems Division
U.S. General Accounting Office
COMPASS is an annual conference committed to bringing together
researchers, developers, and evaluators who work on problems
related to specifying, building, and certifying high-assurance
computer systems. What distinguishes COMPASS from similar
conferences is its emphasis on bridging the gap between research
and practice. Researchers are provided an opportunity to present
results, new theories, and new technologies to both other
researchers and practitioners who can put them to practice. They
can also learn from practitioners of new research problem domains
and of problems encountered in building real systems.
Practitioners have an opportunity to share lessons learned, to
learn of new research, and to influence future research.
Welcome to COMPASS 94, the ninth in a series of annual symposia on
Computer Assurance. This year's conference focuses on both the use
and assessment of formal methods and on alternatives to formal
verification in a variety of critical areas:
* Safety
* Reliability
* Fault Tolerance
* Concurrency and Real Time
* Security
At COMPASS, the diverse program and small conference atmosphere
provide plenty of opportunity for audience and speakers to mingle
and share their experiences. The audience bring their own wealth
of knowledge, and interchanges among industry, members of
government agencies, and academia provide unique opportunities to
discuss current requirements and future needs. We invite you to
participate and increase the benefits of COMPASS by your
attendance. Conference General Co-Chairs: Jarrellann Filsinger,
Committee Booz-Allen & Hamilton and H.O. Lubbes,
NRL
Program Chair: John McLean, NRL
Arrangements: Laura M. Ippolito, NIST
Publications: Ann Boyer, Control Systems
Analysis
Publicity: Paul Anderson, Space and Naval
Warfare Systems Command
Registration: Karen Ferraiolo, Arca Systems,
Inc.
Treasurer: Bonnie P. Danner, TRW Systems
Division
Tutorials: John J. Marciniak, CTA, Inc.
Tools Fair: Charles N. Payne, NRL
Program Committee Paul Ammann, George Mason University
George Dinolt, Loral
Jarrellann Filsinger, Booz-Allen & Hamilton
Virgil Gligor, University of Maryland
Li Gong, SRI International
Connie Heitmeyer, NRL
Jeremy Jacob, University of York
Carl Landwehr, NRL
Teresa Lunt, SRI International
John J. Marciniak, CTA, Inc.
John McDermid, University of York
John McHugh, Portland State University
Jon Millen, MITRE
David Parnas, McMaster University
John Rushby, SRI International
Ravi Sandhu, George Mason University
Jeannette Wing, Carnegie Mellon University
Board of Directors Chair: Dolores R. Wallace, NIST
Vice-Chair: Anthony Shumskas, Logicon, Inc.
Treasurer: Dario DeAngelis, Logicon, Inc.
Secretary: Judy Bramlage, U.S. General
Accounting Office
IEEE AESS: Robert Ayers, ARINC, Inc.
IEEE NCAC: Arthur Cotts
Members: Michael L. Brown, Naval Surface
Warfare Center; Jarrellann Filsinger,
Booz-Allen & Hamilton; Frank
Houston, Weinberg, Spelton, & Sax, Inc.;
H.O. Lubbes, Naval Research Laboratory Agenda COMPASS '94
June 27-July 1, 1994
Monday, 27 June
---------------
8:00 am Registration Opens
9:00 am - 4:00 pm Tutorial (Lunch on your own)
1. "Formal Software Development Using Z"
John McDermid, University of York
Much has been written about the benefit of
formal methods for developing high integrity
software -- but there are relatively few
examples of successful use of formal methods
on large scale projects. This tutorial
demonstrates that cost-effective formal
software development is now possible, using Z
and a refinement approach into Ada that is
supported by two tools: CADiZ and ZETA.
CADiZ supports the production and analysis of
Z specifications. ZETA supports formal,
rigorous or informal stepwise development of
Ada from Z specifications (in compliance with
the UK Interim Defence Standard 00-55) in a
cost-effective way that enables the user to
determine the level of rigor for the
refinement. Examples will be offered, and the
tools will be demonstrated in support of the
presentation.
Tuesday, 28 June
----------------
8:00 am Registration Opens
9:00 am - 4:00 pm Tutorials (Parallel Sessions) (Lunch on your own)
2. "Software System Evaluation and
Certification"
Hans-Ludwig Hausen, GMD (German National
Research Center for Computer Science)
[FULL DAY]
Software quality evaluation and certification
have been recognized as important issues for
the American, European and especially the
Japanese software industry. This tutorial
focuses on the methods and tools for the
evaluation and assessment of software
products and processes. Particular emphasis
is given to identifying and selecting
software characteristics and metrics and the
handling of evaluation methods and tools.
The impact of the SEI Capability Maturity
Model, SPICE, ISO 9000 series, ISO 12119, ISO
9126 and the EVALUATION METHOD will be
discussed in detail.
Tuesday, 28 June (cont.)
----------------
9:00 am - 12 Noon 3. "Software Hazard Analysis"
Nancy Leveson, University of Washington
[HALF DAY]
The goals and techniques of software hazard
analysis will be presented and general
procedures, including new state machine
algorithms, discussed. Topics include
Software System Hazard Analysis and Software
Requirements Analysis. Finally, an example
using a real application (TCAS II) will be offered.
12 Noon - 1:00 pm Lunch (on your own)
1:00 pm - 4:00 pm 4. "Practicing Software Safety in a Virtual
Corporation"
Frank Houston, Weinberg, Spelton, & Sax, Inc.
[HALF DAY]
In this half-day tutorial, the participants
will play the roles of entrepreneurs who are
developing a new medical device. The goal is
for participants to develop the preliminary concept
for the device, including safety requirements.
If time permits, participants will develop a plan
for validation and verification of the device,
addressing regulatory Good Manufacturing Practice
issues in the process.
Wednesday, June 29
------------------
8:00 am Registration and Tools Fair Open (tools that
will be exhibited are listed at the end of this Agenda)
9:30 am - 10:00 am Welcoming Remarks
James H. Burrows, Director, Computer Systems
Laboratory, NIST
Jarrellann Filsinger, General Chair
John McLean, Program Chair
10:00 am - 11:00 am Keynote Address
Jerry O. Tuttle, VADM USN (RET.)
11:00 am - 11:30 am Break
11:30 am - 1:00 pm SAFETY I
"Experience Applying the CoRE Method to the
Lockheed C-130J Software Requirements"
Stuart Faulk, Lisa Finneran, James Kirby
(SPC) and James Sutton (Time Plus)
"AeSOP: An Interactive Failure Mode Analysis
Tool"
Stephen S. Cha (The Aerospace Corp.)
"A Development of Hazard Analysis to Aid
Software Design"
John McDermid and D. J. Pumfrey (University
of York)
2:00 pm - 3:30 pm USE AND ASSESSMENT OF FORMAL METHODS
"Formal Methods in Language Design"
David Guaspari (ORA)
"Case Study: Applying Formal Methods to the
Traffic Alert and Collision Avoidance System
(TCAS)"
Joan J. Britt (MITRE)
"Formal Methods and Dependability Assessment"
V. Stavridou, S. Liu, and B. Dutertre
(University of London)
3:30 pm - 4:00 pm Break
4:00 pm - 5:00 pm ALTERNATIVES TO FORMAL VERIFICATION
"Using Formal Methods to Derive Test Frames
in Category-Partition Testing"
Paul Ammann and Jeff Offutt (George Mason
University)
"Application of an Informal Program
Verification Method to Ada"
Bruce Wieand (IBM) and William E. Howden
(University of California)
5:00 pm Tools Fair Closes
Thursday, June 30
-----------------
8:00 am Registration and Tools Fair Open
9:30 am - 11:00 am FAULT TOLERANCE
"Centurion Software Fault Tolerance Design
and Analysis Tool"
G. Steve Wakefield (SRS), Roger Dziegiel (Air
Force Rome Lab), and Laura L. Pullum (Quality
Research Associates)
"Estimation of Coverage Probabilities for
Dependability Validation of Fault-Tolerant
Computing Systems"
Cristian Constantinescu (Duke University)
"Formal Verification of an Interactive
Consistency Algorithm for the Draper FTP
Architecture Under a Hybrid Fault Model"
Patrick Lincoln and John Rushby (SRI
International)
11:00 am - 11:30 am Break
Thursday, June 30 (cont.)
-----------------
11:30 am - 1:00 am CONCURRENCY AND REAL-TIME SYSTEMS
"State Minimization for Concurrent System
Analysis Based on State Space Exploration"
Inhye Kang and Insup Lee (University of
Pennsylvania)
"Compositional Model Checking of Ada Tasking
Programs"
Jeffrey Fischer (Verdix) and Richard Gerber
(University of Maryland)
"An Ounce of Prevention is Worth a Pound of
Cure: Towards Physically-Correct
Specifications of Embedded Real-Time Systems"
Azer Bestavros (Boston University)
1:00 pm - 2:00 pm Lunch
2:00 pm - 3:30 pm PANEL: SOFTWARE TESTABILITY FOR CRITICAL
SYSTEMS
Dick Hamlet (Portland State University)
William E. Howden (University of California)
Keith Miller (Sangamon State University)
Jeffrey Voas (Reliable Software Technologies
Corp.)
3:30 pm - 4:00 pm Break
4:00 pm - 5:00 pm HARDWARE VERIFICATION
"A Formal Model of Several Fundamental VHDL
Concepts"
David M. Goldschlag (NRL)
"Experiences Formally Verifying a Network
Component"
Paul Curzon (University of Cambridge)
5:00 pm Tools Fair Closes
6:30 pm BANQUET
Speaker: Brian Randell (University of
Newcastle)
Friday, July 1
--------------
8:00 am Registration and Tools Fair Open
Friday, July 1 (cont.)
--------------
9:30 am -11:00 am SAFETY II
"Evaluating Software for Safety Systems in
Nuclear Power Plants"
J. Dennis Lawrence, Warren L. Persons, and G.
Gary Preckshot (Lawrence Livermore National
Laboratory)
"An Approach for the Quality Analysis of
Safety Specifications"
Amer Saeed, Rogerio de Lemos, and Tom
Anderson (University of Newcastle)
"Causality as a Means for the Expression of
Requirements for Safety Critical Systems"
Andrew Coombes, John McDermid, and Philip
Morris (University of York)
11:00 am - 11:30 am Break
11:30 am Tools Fair Closes
11:30 am - 1:00 pm SECURITY
"Covert Channels -- Here to Stay?"
Ira S. Moskowitz and Myong H. Kang (NRL)
"An Experience Modeling Critical
Requirements"
Charles N. Payne, Andrew P. Moore, and David
M. Mihelcic (NRL)
"On Measurement of Operational Security"
Sarah Brocklehurst and Bev Littlewood (City
University) and Tomas Olovsson and Erland
Jonsson (Chalmers University of Technology)
1:00 pm Adjourn Technical Program
Tools Exhibited at Tools Fair
-----------------------------
RiskWatch
AeSOP, ARiES
EVES
AdaWise, Penelope Romulus, Larch-Ada
McCabe Toolset
ModeChart Toolset
Centurion
RDD-100
Boundary Flow Covert Channel Analysis
INTERLOCKS General Information COMPASS '94
June 27-July 1, 1994
Location NIST, located in Gaithersburg, MD, is
approximately 25 miles northwest of
Washington, D.C. The meeting will be held in
the Green Auditorium of the Administration
Building.
Registration NOTE: Members belong to sponsoring or
cosponsoring organizations.
Advanced (before 10 June 1994)
Members Speakers,
Non- One-Day &
Members Members Students
Fee includes coffee breaks, lunches, and
social functions.
Social Functions A banquet with a cash bar and speaker will be
held at the Gaithersburg Hilton on Thursday,
June 30th at 6:30 pm.
Transportation BWI Limo, 301/441-2345, offers commercial van
service from Baltimore-Washington Airport to
Gaithersburg area. Call for reservations.
Airport Transfer Van Service, 301/948-4515,
is available from Dulles International and
Washington National Airports to Gaithersburg.
The Washington Metro has subway service to
Gaithersburg. Metro can be boarded at
Washington National Airport. Take a Yellow
Line train marked "Mount Vernon Square" to
Gallery Place and transfer to a Red Line
train marked "Shady Grove" to Shady Grove.
Service is every 6 to 15 minutes depending on
the time of day. The Shady Grove station is
approximately four miles from the Hilton
Hotel. Contact Hilton for shuttle
information.
General Information (cont.)
Accommodations Conference registration does not include your
hotel reservation. A block of rooms has been
reserved at the Gaithersburg Hilton Hotel,
620 Perry Parkway, Gaithersburg, MD 20877.
The hotel phone number is 301/977-8900. The
special room rate is $70.00 single or double.
To register for a room, please use the
enclosed hotel reservation form and send it
directly to the hotel no later than June 12,
1994. After that date the rooms will be
released for general sale at the prevailing
rates of the hotel.
Registration Karen Ferraiolo
Information COMPASS '94 Registration
Arca Systems, Inc
8229 Boone Blvd, Suite 610
Vienna, VA 22182
Phone: 703/734-5611
Fax: 703/790-0385
Technical John McLean
Information Naval Research Laboratory
Code 5543
4555 Overlook AV, SW
Washington, DC 20375
Phone: 202/767-3852
Fax: 202/404-7942
Driving From northbound I-270 take Exit 10, Rt. 117
West, Clopper Road. At the first light on
Clopper Road, turn left on to the NIST
grounds. From Southbound I-270 take Exit
11B, Route 124 West, Quince Orchard Road. At
the second light turn left on to Clopper
Road. At the first light on Clopper Road,
turn right on to the NIST grounds. To reach
the Administration Building, turn left after
passing the guard office. Signs will direct
you to visitor parking.
Transportation will be provided to and from
the Gaithersburg Hilton and NIST Monday
through Thursday. Conference COMPASS '94
Registration June 27-July 1, 1994
Card
Advance Registration (Before 10 June 1994)
_____Conference Registration (includes 1 copy of proceedings)
_____Proceedings Only
_____Extra Proceedings _____ copies
_____Tutorial #1 - Formal Software Development Using Z
_____Tutorial #2 - Software System Eval. and Certification
_____Tutorial #3 Software Safety and #4 Hazard Analysis
Name______________________________________________________
Company___________________________________________________
Street Address____________________________________________
Rm. No./Mail Code_________________________________________
City, State, ZIP__________________________________________
Country___________________________________________________
Business Telephone________________________________________
IEEE Membership No._______________________________________
Co-Sponsor Name___________________________________________
Total Amount US $_________________________________________
_____Check here is you will be using the shuttle to and from the
Hilton and NIST (free!).
_____Check enclosed made payable to COMPASS '94.
(Checks from outside the USA must be written on a USA bank.)
Request for refunds after 10 June 1994 will be subject to a $15
administrative fee.
"In reviewing the Institute for Electrical and Electronics
Engineers' plans for COMPASS Conferences, The Assistant Secretary
of Defense (Public Affairs) finds this event meets the standards
for participation by DoD personnel under instruction 5410.20 and
DoD Standards of Conduct Directive 5500.7. This finding does not
constitute DoD endorsement of attendance which must be determined
by each DoD component."
Place Conference Registration Card in envelope and mail to:
Karen Ferraiolo
COMPASS '94 Registration
Arca Systems, Inc
8229 Boone Blvd, Suite 610
Vienna, VA 22182 Hotel COMPASS '94
Registration June 27-July 1, 1994
Card
Number of Persons___________________________________________
Rate $70 single or double (apply 12% tax to rate). All
reservations must be received by 12 June 1994. All room
reservations must be guaranteed by a one-night deposit.
Deposit will guarantee first night availability, and will be
credited to last night of reservation. Deposit refunded if
request received 48 hours prior to reserved arrival.
_____ Check enclosed made payable to The Gaithersburg
Hilton
_____ One night deposit enclosed $___________________