First Announcement COMPASS '94 Ninth Annual Conference On Computer Assurance 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) Wednesday, June 29 (cont.) ------------------ 1:00 pm - 2:00 pm Lunch 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 Conference 250 315 100 Tutorial (per day) 80 110 Proceedings Only 20 30 20 On-Site (after 10 June 1994) Members Speakers, Non- One-Day & Members Members Students Conference 300 375 100 Tutorial (per day) 80 110 Proceedings Only 20 30 20 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.) _____MasterCard No._____________________________Exp._____ _____VISA Card No.______________________________Exp._____ _____Diners Club No.____________________________Exp._____ _____American Express No._______________________Exp._____ Authorized Signature_____________________________________ 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 Hilton Hotel, 301/977-8900 Name________________________________________________________ Company_____________________________________________________ Street Address______________________________________________ Rm. No./Mail Code___________________________________________ City, State, ZIP____________________________________________ Country_____________________________________________________ Business Telephone__________________________________________ Arrival Date________________________________________________ Departure Date______________________________________________ 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 $___________________ Guaranteed by_______________________________________Exp._____ Card No._____________________________________________________ Authorized Signature_________________________________________ Please place in envelope and mail to: The Gaithersburg Hilton 620 Perry Parkway Gaithersburg, MD 20877