HILT 2014             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Saturday Full-Day Tutorials (9:00am - 5:30pm)

SAT_FD_1: Object-Oriented Programming with Ada 2005 and Ada 2012
Ed Colbert (Absolute Software)

Level: Intermediate
Part 1 (Morning) : Understanding of OO concepts and Ada 83
Part 2 (Afternoon) : Understanding of Ada 95's OO Support (or attending morning sessions)

Ada 05 makes it easier to learn and use object-oriented programming (OOP) than Ada 95, as well integrating OOP with concurrent programming. Ada 2012 makes small changes to the OOP model of Ada 05's that facilitate its use, and that make it easier for the compiler to detect errors. Ada 2012 also adds contracts that allow the OO programmer to define the perceived behavior of a tagged type and at the same time constrain the behavior of derived types.

Outline

Part 1 (Morning) of this tutorial will look at the following topics.

SAT_FD_2: Introduction to SPARK 2014
Peter Chapin (Vermont Technical College), John W. McCormick (University of Northern Iowa)

Level - Intermediate. Prerequisites are knowledge of Ada (but not necessarily Ada 2012) and some basic familiarity with the concepts of static analysis.

People wishing to learn more about the SPARK 2014 language and the opportunities it offers for novel verification techniques should attend. Attendees may be involved in or interested in new techniques for the engineering of safety- or security-critical applications or interested in languages and methods suitable for reducing post-delivery defect rates in consumer products.

SPARK 2014 is the latest evolution of the SPARK programming language. Based on Ada 2012, it encompasses a larger subset of the Ada language than its predecessors. It uses Ada 2012 syntax rather than special annotations for additional contracts used for advanced static verification techniques.

Topics covered in this full day tutorial include:

  1. SPARK 2014 rationale
  2. Ada 2012 constructs used by SPARK 2014
  3. SPARK dependency contracts
  4. Proof
  5. Interfacing with SPARK
  6. Proof and testing

Bring your laptop computer as we will include several hands-on exercises. We can help you install GNAT GPL 2014 and SPARK GPL 2014.

Sunday Morning Tutorials (9:00am - 12:30pm)

SUN_AM_1: High-Integrity Object-Oriented Programming with Ada 2012
Ben Brosgol (AdaCore)

Level: Knowledge of some Object-Oriented language is assumed, and experience with the OO features of Ada 95 will be useful. Familiarity with the new Ada 2012 features, or with software certification standards such as DO-178B/C, is not required.

Object-Oriented Programming (OOP) has been successfully used for developing many kinds of software because of its benefits in maintainability and reuse. However, until recently it has not made much traction among developers of High-Integrity systems -- i.e., where high levels of safety and/or security are required. This tutorial, based on the Object-Oriented Technology and Related Techniques supplement (DO-332) to the DO-178C standard for commercial airborne systems, will describe the issues that arise with OOP in High-Integrity systems and show how they can be addressed in Ada 2012. Among the topics to be covered is the interaction between OOP and contract-based programming, in particular how Ada 2012 accommodates the Liskov Substitution Principle for class inheritance.

Reasons for attending

Attendees will learn how to anticipate and avoid the various "traps and pitfalls" associated with OOP in safety-critical or high-security software, and how to use Ada 2012 to write OO programs that can comply with software standards such as DO-178C.

Sunday Afternoon Tutorials (2:00 - 5:30pm)

SUN_PM_1: AADLv2, An Architecture Description Language for the Analysis and Generation of Embedded Systems
Jérôme Hugues (Institute for Space and Aeronautics Engineering (ISAE), Toulouse, France), Frank Singhoff (Université de Bretagne, Brest, France)

Beginning to intermediate. Some experiences on real-time embedded systems design and implementation would be useful.

The Architecture Analysis and Design Language (AADL) is an SAE International Standard dedicated to the precise modeling of complex embedded systems, covering both hardware and software concerns. Its definition relies on a precise set of concepts inherited from industry and academics best practice: clear separation of concerns among layers, rich set of properties to document system metrics and support for many kind of analysis: scheduling, safety and reliability, performance, but also code generation.

In this tutorial, we will provide an overview of AADLv2 and illustrate how several analyses can be combined on an illustrative example: a UAV platform.

The tutorial will illustrate the two key dimensions of AADL: 1) a modeling process, following a system engineering approach: elicitation of high-level requirements and corresponding architecture, refinements and then full implementation, 2) connection with various analysis down and up the traditional engineering V-cycle. The tutorial will cover both language and state-of-theart tools: OSATE2, Cheddar and Ocarina and connections with other tools like Simulink, OpenFTA.

We will illustrate how to merge various modeling and analysis concerns using AADL: validation of mission-level objectives, high-level system validation, verification of schedulability and reliability and then discuss alternatives to generate part of the system.

Motivation for the tutorial

AADL is notation which is part of the model-based families, along with OMG SysML, MARTE or AutoSAR. It has been defined with a strong focus on analysis capabilities from its inception, while being versatile enough to be applied to a wide set of embedded systems. European projects (FP5-ASSERT, TASTE, Flex-eWare), but also US projects (SAVI, Meta) demonstrated that AADL could help engineers in their design effort in the space, avionics and embedded domains.

In the mean time, the academic community adopted AADL as a conveyor to bind numerous tools, covering model checking, scheduling, power evaluation or simulation capabilities to name a few. The AADL committee pages at https://wiki.sei.cmu.edu/aadl/index.php/AADL_Related_Publications lists more than 200 publications around AADL illustrating the variety of analysis being implemented.

The motivation of the tutorial is two-fold: 1) to underline the value of model-based as a viable solution to support design activities of embedded systems, but also 2) to illustrate how to extend AADL capabilities to meet specific project requirements.

The tutorial will cover the following topics:

  1. Introduction to the AADL, history and key concepts (1 hour)
  2. Presentation of the UAV platform, analysis challenges (30 minutes)
  3. How to map AADL concepts onto an analysis domain, illustrations on a scheduling analysis (45 minutes)
  4. From model to code: code generation strategies, connection with external behavioral models (Simulink) and code (45 minutes)

All topics will be illustrated through demonstration of tools; the models and the tools will be made available to participants and on author's pages.

Form of the tutorial

The tutorial will have the form of a lecture, with hand-outs and tools made available to participants. We will not ask participants to run the tools, but instead rely on interactive discussion while enriching the various models. Howeve, if participants bring a laptop computer. We may provide them several AADL tools (e.g. ocarina, Cheddar, ...) for some hands-on exercises/demos.

SUN_PM_2: Rust — Zero-Cost Safety
Niko Matsakis (Mozilla Research)

Rust is a new programming language targeting systems-level applications. Rust offers a similar level of control over performance to C++, but guarantees type soundness, memory safety, and data-race freedom. One of Rust's distinguishing features is that, like C++, it supports stack allocation and does not require the use of a garbage collector.

This tutorial will cover:


Created on 14 October 2014;  website comments and corrections to ClydeRoby at ACM.Org