Tutorials

Improve the benefits of coming to the conference further by attending our tutorials, all given by well-known experts.

Morning tutorial sessions run from 09:30 to 13:00, with a break 11:00-11:30. Afternoon tutorial sessions run from 14:30 to 18:00 with a break 16:00-16:30.

T1 - Introduction to SPARK 2014

Peter Chapin, Vermont Technical College

This tutorial will provide an introduction to the SPARK 2014 language and tools, covering all the major features of SPARK to date. New features, such as support for concurrency and Liskov Substitution Principle (LSP) verification, will be presented. The goal of the tutorial is to give attendees enough background so that they can explore using SPARK in real projects. The focus will be on the practical application of SPARK rather than on the theory. Topics such as mixed language programming, the interaction between proof and testing, and approaches for debugging proofs will also be included. Hands-on exercises will be provided. Attendees should bring a computer with the GNAT GPL and SPARK GPL editions installed. These are available for download from libre.adacore.com/download/.

Reasons for attending

• Learn about SPARK 2014 and what it can (and cannot) do.
• Know how to use SPARK in an upcoming or existing project.
• Understand how SPARK works in the “real world”.

Presenter

Peter Chapin is a professor of software engineering at Vermont Technical College (VTC) in the US, where he has taught Ada and SPARK to undergraduate and graduate students. He is a co-author, with John McCormick, of Building High Integrity Applications with SPARK. Dr. Chapin has been the software director at VTC’s CubeSat Laboratory since 2009 where he has overseen the development of CubeSat flight software in SPARK written by students.

T2 - Ada on ARM Cortex-M, a zero-run-time approach

Maciej Sobczak, GE Aviation and Inspirel

ARM Cortex-M is a core design used by multiple families of microcontrollers available from various vendors. Due to their performance vs. price ratio and a relatively elegant architecture, Cortex-M has become a de-facto standard among designers of final embedded devices. Ada programmers can target this family and benefit from available tool chains, relying on several run-time bases. This tutorial presents the zero-run-time approach, in which the programmer supplies the entire software part and benefits from minimal image size as well as seamless integration with software modules written in C. Topics to be covered include why Ada on ARM Cortex-M, the current landscape and available solutions, memory layout, linking and loading, Ada constructs for managing registers, interrupts, and interfacing with C

Reasons for attending

• Learn the basic concepts of applying Ada on ARM Cortex-M microcontrollers
• See how common integration deployment problems can be solved or circumvented.
• Understand the pros and cons of a zero run-time approach.

Level

Introductory. The tutorial is intended for programmers at any level of Ada proficiency (including beginners) who are interested in embedded systems, and “makers” in particular.

Presenter

Maciej Sobczak works for GE Aviation and is also a founder of Inspirel in Poland, a company focused on reliable software methods. He has consulted in the area of distributed systems, performance-oriented C++ programming and mixed-language techniques. Mr. Sobczak has conducted training on Ada, and his book "Ada and SPARK on ARM Cortex-M" is available on-line.

T3 - Software Measurement for Dependable Software Systems

William Bail, The MITRE Corporation

Software measurement allows developers to monitor key attributes of their software products and their applied processes Such monitoring is crucial to successful implementation and to avoiding surprises late in the system development. Applying and interpreting measures is key. Poor choices can result in wasted effort and misleading indicators. This tutorial surveys the range of popular and effective measures, and provides guidelines for their selection, application, and interpretation.

Reasons for attending

• Understand the role of software measures and their role in supporting management of software development projects.
• Learn the different categories of measures and how to select specific measures.
• Know how to establish and conduct an effective metrics program.

Level

Intermediate. Attendees should be familiar with software and code development and have some experience in software measurement.

Presenter

Dr. Bail is a Computer Scientist in the Software Engineering Center at The MITRE Corporation in the US. His technical areas of focus include dependable software design and assessment, metric definition and application, error handling policies, design methodologies, and verification and validation. Dr. Bail has taught computer science courses at the University of Maryland and has presented tutorials on software engineering at international conferences.

T4 - Real-Time Parallel Programming with the UpScale SDK

Luis Miguel Pinho, ISEP and Eduardo Quinones, BSC

Nowadays, the prevalence of computing systems in our lives is so ubiquitous that it would not be far-fetched to state that we live in a cyber-physical world dominated by computer systems. These systems demand for more and more computational performance to process large amounts of data from multiple data sources, some of them with guaranteed processing response times. In other words, systems are required to deliver their results within pre-defined (and sometimes extremely short) time bounds. Examples can be found for instance in intelligent transportation systems for fuel consumption reduction in cities or railway, or autonomous driving of vehicles.

To cope with such performance requirements, chip designers produced chips with dozens or hundreds of cores, interconnected with complex networks on chip. Unfortunately, the parallelization of the computing activities brings many challenges, among which how to provide timing guarantees, as the timing behaviour of the system running within a many-core processor depends on interactions on shared resources that are most of the time not know by the system designer.

P-SOCRATES (Parallel Software Framework for Time-Critical Many-core Systems) was a FP7 European project, which developed a novel methodology to facilitate the deployment of standardized parallel architectures for real-time applications. This methodology was implemented (based on existent models and components) to provide an integrated software development kit (the UpScale SDK) to fully exploit the huge performance opportunities brought by the most advanced many-core processors, whilst ensuring a predictable performance and maintaining (or even reducing) development costs of applications. The tutorial will provide an overview of the project methodology and SDK, and will include a final open discussion to the floor on its applicability to Ada.

Reasons for attending

• Learn how to achieve time-predictability in parallel computation.
• Learn the basics of the UpScale SDK tools for the development of real-time parallel applications.
• Participate in the process of analyzing the use of OpenMP with Ada

Level

Intermediate. Attendees should have knowledge of software development for embedded systems.

T5 - Using Gnoga for Desktop/Mobile GUI and Web development in Ada

Jean-Pierre Rosen, Adalog

Gnoga is a framework / toolset for developing GUI and Web applications using Ada. Not to be confused with web development frameworks compensating for stateless client/server connections to attempt to create usable UIs, Gnoga uses a bidirectional websocket connection allowing the browser to function as a live rendering engine with instant real-time response both locally for desktop GUI applications and remotely over the web. Gnoga’s framework allows rapid development of client server desktop, mobile and cloud applications and is far more capable for web application development than any existing framework regardless of language. Gnoga is open source under the “non-viral” GPLv3 with runtime exceptions and may be used for proprietary as well as free applications.

This tutorial provides a detailed overview of Gnoga, its structure, its principles, and how to use it for Web, mobile and local (desktop and embedded) applications.

Reasons for attending

• Understand how to make GUI applications in Ada independently of the host system (Windows, Mac, Linux).
• Learn how to use the same tools and framework for desktop, mobile and web applications.

Level

Intermediate. Attendees should have a casual knowledge of Ada.

Presenter

JP Rosen is a professional teacher, offering training in Ada since 1979 (when it was preliminary Ada!), methods, and software engineering. He runs Adalog, a French company that provides training, consulting, and services in all areas connected to the Ada language and software engineering. He is chairman of AFNOR’s (French standardization body) Ada group, AFNOR’s spokeperson at WG9,a member of the Vulnerabilities group of WG9, and chairman of Ada-France.

T6 - Frama-C, a Collaborative Framework for C Code Verification

Julien Signoles, CEA LIST

Frama-C is an extensible source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance with a common formal specification language named ACSL.

This tutorial on Frama-C takes participants on a journey into the Frama-C world along its main plug-ins: the deductive verification tool WP, the abstract-interpretation based plug-in Eva, and the run-time verification tool E-ACSL. It also includes a presentation of the formal specification language ACSL and emphasizes possible collaborations between these plug-ins and a few others. The presentation is illustrated with concrete examples of C programs.

Reasons for attending

• If you don’t know formal methods: learn how to use them in practice without doing any math.
• If you already know formal methods and a verification tool for another programming language (e.g. SPARK 2014): learn a state-of-the-art tool currently used in practice for verifying critical C software.

Level

Introductory to intermediate. Attendees should know the C programming language but need not have any experience with formal methods.

Presenter

Julien Signoles is a research engineer at CEA LIST’s Software Security and Reliability Lab in France and one of the main developers of Frama-C. His research focuses on run-time assertion checking, software security, and applications of program analysis techniques. Dr. Signoles has delivered tutorials and provides professional training on Frama-C and its plug-ins.

T7 - On beyond ASCII: Characters, Strings, and Ada 2012

Jean-Pierre Rosen, Adalog

Characters represent an incredibly difficult issue, in general and in programming languages. The extent of the problems is hard to appreciate, as seen from the English language which needs only simple characters, but becomes apparent when you consider accented letters, ideograms, and even music notes or Klingon… This tutorial explains all the issues with characters: their encoding and representation (both internally and externally), the various standards (ISO 10646, Unicode, UTF, …) collating sequences, etc. In addition, it addresses character strings in programming languages in general, and in Ada 2012 in particular, showing why various forms of strings are provided and how to use them.

Reasons for attending

• Understand (at last!) the issues with characters and the precise meaning of confusing notions like code-points, encoding, character sets, etc.
• Learn how to account for character issues in your Ada programs.
• Understand the differences between the various kinds of strings provided by Ada, and be able to choose the most appropriate one according to your needs.

Level

Intermediate. Attendees should have a casual knowledge of Ada.

Presenter

JP Rosen is a professional teacher, offering training in Ada since 1979 (when it was preliminary Ada!), methods, and software engineering. He runs Adalog, a French company that provides training, consulting, and services in all areas connected to the Ada language and software engineering. He is chairman of AFNOR’s (French standardization body) Ada group, AFNOR’s spokeperson at WG9,a member of the Vulnerabilities group of WG9, and chairman of Ada-France.

T8 - Modular Open System Architecture for Critical Systems

William Bail, The MITRE Corporation

A recent key design strategy is the use of open modular systems. Understanding the underpinnings of open systems, its benefits, and its implementation is essential to being able to dependably develop such software systems. This tutorial examines the concepts of modular open software design and architecture, and the motivation for following this approach. The tutorial also correlates the benefits achievable with such approaches to the attributes of such designs. It describes examples of good and faulty design, and present a variety of design challenges that are commonly encountered in realizing a modular open design.

Reasons for attending

• Understand the concepts of open modular design.
• Learn its benefits and drawbacks, and practical guidance on how to achieve, including trade-offs and challenges.

Level

Intermediate/Advanced. Attendees should have knowledge of software system design.

Presenter

Dr. Bail is a Computer Scientist in the Software Engineering Center at The MITRE Corporation in the US. His technical areas of focus include dependable software design and assessment, metric definition and application, error handling policies, design methodologies, and verification and validation. Dr. Bail has taught computer science courses at the University of Maryland and has presented tutorials on software engineering at international conferences.