ASE 2002 Tutorials, 24 September 2002

Tutorials will take place in rooms 1.82 and 1.83 of the


Department of Computing and Electrical Engineering

Heriot-Watt University

Riccarton Campus

Edinburgh EH14 4AS




For information on how to reach the venue, see here.



T3: From Research to Industry: The Role of Software Engineering Standards


T3: From Research to Industry: The Role of Software Engineering Standards







T2: Methods and Techniques for Industrial Strength Software Engineering

T4: Software Model-Checking





T2: Methods and Techniques for Industrial Strength Software Engineering

T4: Software Model-Checking

Tutorial 2: Methodologies and Technologies for Industrial Strength Systems Engineering

Presented by: Marina Walden and Elena Troubitsyna

Aabo Akademi University,


MATISSE (Methodologies and Technologies for Industrial Strength Systems Engineering), is a European Framework 5 project. The core objective of the MATISSE project is the development of industrial-strength methodologies and associated technologies for the engineering of software-based critical systems. Key outputs of this project will be a freely available Methodology Handbook, and tutorials illustrated by experience with industrial case studies. In this tutorial a healthcare case study will be used to illustrate how established system safety techniques are integrated into a formal development for an industrial system using B.

The healthcare case study deals with the development of a safety-critical drug discovery system, Fillwell. It should guarantee an extremely high precision and a constant level of quality on the experiments to be performed. Even if the direct harm to the humans using the system is quite moderate, the indirect harm caused by the results of incorrectly performed experiments could be catastrophic. Hence, safety and reliability are important issues for this system. In the past few years regulatory requirements for drug discovery systems have tightened. Due to this there is a need to introduce formal methods in the development lifecycle to prepare for future regulations.

Tutorial 3: From Research to Industry: The Role of Software Engineering Standards

Presented by:

Stacy Nelson (1), Michael Whalen (2), Charles Pecheur (3)

(1)NelsonConsult / NASA Ames

(2)University of Minnesota



The tutorial will explain the role software engineering standards play during technology transfer from research systems/software to industry applications. It will provide an overview of the following standards:

  • IEEE/EIA 12207 (Software Life Cycle Processes published in 1998 by Institute of Electrical and Electronics Engineers Electronic Industries Association)
  • NASA Standards (NASA Procedures and Guidelines (NPG) 2820.DRAFT, NASA Software Guidelines and Requirements and NASA Procedures and Guidelines (NPG) 8730.DRAFT 2, Software Independent Verification and Validation (IV&V) Management)
  • DO-178B (Certification of Airborne Software)
  • Comparison of standards (MIL STD 498, 2167A, Capability Maturity Model (CMM))

Following these software engineering standards is essential to developing safety critical systems and software like the aerospace systems onboard spacecraft and aircraft. Real world examples of the application of V&V standards will be provided to illustrate use of standards for both traditional software development and advanced software development requiring formal verification methods (model checking). Examples include:

  • Traditional testing used during development of military software
  • Formal verification for Integration Vehical Health Management (IVHM) for the 2nd Generation RLV (new space shuttle) [1] [2]>
  • Formal verification for Intelligent Flight Control System (IFCS) for F-15 [3]

[1] see
[2] Charles Pecheur, Reid Simmons. From Livingstone to SMV: Formal Verification for Autonomous Spacecrafts. First FAABS Workshop, LNCS 1871, Springer Verlag.
[3] see

Tutorial 4: Software Model-Checking

Presented by: Willem Visser

NASA Ames Research Center
Moffett Field, California, USA


Applying model checking to analyze software, or more specifically programs, has become very popular in the last 5 years. Model checking has always been actively used in the analysis of hardware systems and protocols, but this new trend to focus on programs written in popular programming languages such as C, C++ and JAVA, makes model checking relevant to a potentially much larger user community. The aim of this tutorial is to introduce model checking for the analysis of programs.

The tutorial will start with a brief introduction to model checking and how it evolved over the last 2 decades into a technique that not only is a mainstay in the hardware industry, but is also actively used within large software driven organizations such as Microsoft. The main part of the tutorial will focus on the analysis of programs with model checking:

  1. history of this new field, including an introduction of the main research groups in the field
  2. the major research issues in the field
  3. how techniques from static analysis, such as abstract interpretation and slicing, is used during model checking
  4. overview of the tools currently available (SPIN and extensions, Java PathFinder, Bandera, SLAM, etc.).

The last part of the tutorial will discuss some of the applications in using model checking to analyze programs: DEOS real-time operating system (Honeywell), Remote Agent spacecraft controller (NASA) and the K9 Mars rover (NASA).

The tutorial will be aimed at both industrial and academic participants. It is our hope that after this tutorial industrial participants will be able to judge the maturity of the field and how it will fit into their immediate and long-term needs, whereas for academic participants, we hope the tutorial will serve as an introduction into a new and exciting field with many open research issues.


Currently Maintained by Cecilia Mascolo (

Website hosted by the Software Systems Research Group / Dept. of Computer Science / UCL