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
Scotland
UK
For information on how to reach the venue, see here.
Schedule:
|
0930-1100 |
T3: From Research to Industry: The Role of Software Engineering Standards Coffee T3: From Research to Industry: The Role of Software Engineering Standards |
|
|
1100-1130 |
||
|
1130-1245 |
||
|
1245-1345 |
Lunch |
Lunch |
|
1345-1515 |
T2: Methods and Techniques for Industrial Strength Software Engineering |
|
|
1515-1545 |
Coffee |
Coffee |
|
1545-1700 |
T2: Methods and Techniques for Industrial Strength Software Engineering |
|
Presented by: Marina Walden and Elena Troubitsyna
Aabo Akademi University,
Finland
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.
Presented by:
Stacy Nelson (1), Michael Whalen (2), Charles Pecheur (3)
(1)NelsonConsult / NASA Ames
(2)University of Minnesota
(3)RIACS/NASA Ames
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:
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:
[1] see http://ase.arc.nasa.gov/vvivhm
[2] Charles Pecheur, Reid Simmons. From Livingstone to SMV: Formal Verification
for Autonomous Spacecrafts. First FAABS Workshop, LNCS 1871, Springer Verlag.
[3] see http://ase.arc.nasa.gov/VVAdaptive/
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:
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.
Website
hosted by the Software
Systems Research Group / Dept.
of Computer Science / UCL