Tutorials

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

Tutorials will take place Monday, June 18^th, and Friday, June 22^nd. Morning tutorial sessions run from 09:30 to 13:00, with a break 11:00-11:30. Afternoon tutorial sessions run from 14:00 to 17:30 with a break 15:30-16:00.

T1 - Recent Developments in SPARK 2014

Peter Chapin, Vermont Technical College

Location: Ruby 2 Room

This tutorial will quickly cover the basics of SPARK 2014 for the benefit of those attendees who have no SPARK 2014 experienced (assumed to be the majority of the attendees). This overview will not cover every detail of SPARK. Instead it will provide the necessary background so that the newer features of SPARK can be understood. The bulk of the time will focus on the newer features that have been added to SPARK in recent years, along with some general comments about where SPARK development may be heading in the future. Sample code will be provided in machine readable form, so attendees can experiment with SPARK first hand during allocated “lab” times during the tutorial. Attendees are encouraged to bring a computer.

Level: Intermediate

Attendees should have working familiarity with Ada including exposure to, but not necessarily expertise with, Ada’s concurrency and object-oriented features, but no prior experience with SPARK is required. Experienced SPARK users who are interested in the SPARK’s newer features are also welcome.

Reasons for attending

Attendees will leave the tutorial with a general understanding of SPARK’s abilities and of the direction SPARK development has been moving. Attendees will be in a good position to explore SPARK further by trying it on their own projects.

Presenter
 
Dr. Chapin is a professor of software engineering at Vermont Technical College (VTC) in the United States. He has been a faculty member there for 32 years and has taught both Ada and SPARK to undergraduate and graduate students. He is a co-author, along with John McCormick, of "Building High Integrity Applications with SPARK", published by Cambridge University Press in 2015. Dr. Chapin has been the Software Directory at VTC’s CubeSat Laboratory since 2009 where he has overseen the development of CubeSat flight software in SPARK done by students

T2 - Access types and memory management in Ada 2012

Jean-Pierre Rosen, Adalog

Location: Ruby 3 Room

In most languages, pointers are either low-level (pure hardware addresses in C), or implicit (Java, C#). Ada provides explicit pointers, but of a higher level of abstraction (hence the use of the term “access”), disconnected from the hardware level, and as safe as possible. In addition, the language includes sophisticated features for controlling memory allocation and deallocation. While this has great benefits, it may confuse those who are used to pointers in other languages. Proper usage also requires some difficult to grasp notions, like accessibility levels. This tutorial explains all the issues with Ada access types, from basic usage to sophisticated features like remote access types. Many practical examples demonstrate how to use them and how to control memory allocation, and special emphasis is provided for the latest features offered by Ada 2005 and 2012. A must-attend for all those using access types.

Level: Intermediate

Expected audience experience: Casual knowledge of Ada.

Reasons for attending

• Understand what makes Ada access types different from other languages’ pointers;
• Explore rarely taught issues, like accessibility levels, storage pools and subpools, remote access types...;
• Learn when and how to use access types – and when not to use them.

Presenter
 
J.P. Rosen is a professional teacher, teaching Ada (since 1979, it was preliminary Ada!), methods, and software engineering. He runs Adalog, a company specialized in providing training, consultancy, 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, member of the Vulnerabilities group of WG9, and chairman of Ada-France. Adalog offers regularly on-site and off-site training sessions in Ada. This tutorial is based in part on the “advanced Ada’ course offered by Adalog.

T3 - Design and architecture guidelines for trustworthy systems

This tutorial was cancelled due to the unforeseen unavailability of the presenter for health reasons. We apologise for any inconvenience this may cause.

William Bail, The MITRE Corporation

Software design and architecture together play a central role in software development. Understanding their concepts and principles is essential to being able to develop a trustworthy and dependable software system. This tutorial examines these concepts, discusses design quality attributes necessary to ensure trustworthy behaviour, and provides an overview of different design approaches. It will differentiate architecture and design, their relationship to coding styles, and describe examples of good and faulty design. It will introduce a variety of design challenges that are commonly encountered and will discuss the impact of complexity in the quality of the software, recognizing that complexity presents significant risk to the dependable design understood by developers. Design features need to be correlated to counteract potential threats to security and safety. All designs have inherent properties, but not all designs have the same properties, resulting in a need to select a design for a system that is coherent with the system’s intended role and usage profile

Level: Intermediate / Advanced

Targeted at practitioners who are involved in designing and developing complex systems which have high dependability and trust requirements.

Reasons for attending

The tutorial will provide present a perspective on the roles of design and architecture in the development of software intensive systems that have safety and cyber-secure roles, and will provide guidance on how to approach such development. As such, it will directly support process improvement, and provide a basis for achieving trustworthy performance. It emphasizes the role of design features that enhance achieving desirable dependability goals. It recommends practical approaches for soliciting and documenting deriving and documenting design features.

Presenter
 
Since 1990, Dr. Bail has worked for The MITRE Corporation in McLean VA as a Computer Scientist in the Software Engineering Center (SWEC). MITRE is a not-for-profit corporation chartered to provide systems engineering services to the U.S. Government agencies, including the DoD, the FAA, and the IRS. Within MITRE, the SWEC focuses on supporting various programs with consultation, particularly transitioning emerging technologies into practice. Dr. Bail has been involved with establishing modular open system guidance and policy for multiple customers.

Dr. Bail's technical areas of focus include dependable software design and assessment, metric definition and application, error handling policies, techniques for software specification development, design methodologies, metric definition and application, and verification and validation. Prior to 1990, Dr. Bail worked at Intermetrics Inc. in Bethesda MD.

From 1989 to 2011, he served as a part-time Adjunct Professor at the University of Maryland University College where he developed instructional materials and taught courses in software engineering, in topics such as Software Requirements, Verification and Validation, Software Design, Software Engineering, Fault Tolerant Software, and others. Previously, Dr. Bail taught part-time at The University of Maryland from 1983-1986 in the Computer Science Department for undergraduate courses in discrete mathematics, computer architecture, and programming language theory.

Dr. Bail has presented tutorials on Cleanroom Software Engineering, Semi-Formal Development Techniques, Statistical Testing, Verification and Validation, and Requirements Engineering at SIGAda, AdaEurope, NDIA Systems Engineering Conference, and other conferences.

Dr. Bail received a BS in Mathematics from Carnegie Institute of Technology, and an MS and Ph.D. in Computer Science from the University of Maryland.

T4 - Numerics for the Non-Numerical Analyst

Jean-Pierre Rosen, Adalog

Location: Ruby 3 Room

Numerics are a special area of software development, and numerically intensive programs are best developed by specialists of the domain. On the other hand, many programs have to deal with mathematical computations, without being really numerically intensive.

This tutorial addresses the techniques (and pitfalls) that every application developer needs to know as soon as there are some computations that go beyond simple integer arithmetic, without requiring them to be advanced numerical analysts. The tutorial also addresses the various tools offered by Ada, from numeric types to libraries.

Level: Intermediate

Expected audience experience: Casual knowledge of Ada.

Reasons for attending

• Learn how to select the most appropriate numeric type for your applications;
• Avoid pitfalls and increase the accuracy and portability of numeric computations;
• Discover the standard libraries provided by Ada.

Presenter
 
J.P. Rosen is a professional teacher, teaching Ada (since 1979, it was preliminary Ada!), methods, and software engineering. He runs Adalog, a company specialized in providing training, consultancy, 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, member of the Vulnerabilities group of WG9, and chairman of Ada-France. Adalog offers regularly on-site and off-site training sessions in Ada. This tutorial is based in part on the “advanced Ada’ course offered by Adalog.

T5 - Requirements development for safety and security critical systems

This tutorial was cancelled due to the unforeseen unavailability of the presenter for health reasons. We apologise for any inconvenience this may cause.

William Bail, The MITRE Corporation

The requirements defined for a system form the foundation for the development of the system, and as such, are fundamentally core to the successful realization and delivery of the system to the eventual users. Cost and schedule increases in the development of systems, and shortcomings in deployed systems are closely correlated to weaknesses in the system’s requirements. Some historic data suggests that requirements are responsible for nearly half of all system development failures. For dependable systems, shortcomings in requirements development have an especially dramatic impact. For example, systems requiring a high level of security are often not addressed until later in the development process. This tutorial discusses shortcomings in current practices, and provides guidance for enhanced practices that address historic shortcomings. It also provides an approach to weighing trade-offs associated with ambitious goals and realistic limits, and recognizes the complex and multiple interplays between different requirements. It specifically addresses the issue of stakeholder acceptability, allowing trade-offs of various system qualities to determine overall system acceptance. It also emphasizes the tight relationship between design and requirements development, showing how good practice can directly improve the quality of the resulting system. The tutorial describes the ways that requirements need to be handled to maximize the likelihood of success. This tutorial has been updated significantly from versions presented at previous Ada-Europe conferences.

Level: Intermediate / Advanced

Targeted at practitioners who are involved in developing complex systems which have high dependability and trust requirements.

Reasons for attending

The tutorial will provide a framework for development of requirements for cyber and safety critical systems and provide advice on how to approach such development. As such, it will directly support process improvement, and provide a basis for a predictable and reliable requirements development activity. It justifies the level of attention that needs to be placed on the development and maturation of system and software requirements. It supports obtaining a perspective against which requirements can be viewed and suggests practical approaches for soliciting and documenting requirements. It will explain the underlying basis for how requirements need to be handled and will provide solutions for some commonly-encountered challenges when developing requirements for large, software-intensive systems.

Presenter
 
Since 1990, Dr. Bail has worked for The MITRE Corporation in McLean VA as a Computer Scientist in the Software Engineering Center (SWEC). MITRE is a not-for-profit corporation chartered to provide systems engineering services to the U.S. Government agencies, including the DoD, the FAA, and the IRS. Within MITRE, the SWEC focuses on supporting various programs with consultation, particularly transitioning emerging technologies into practice. Dr. Bail has been involved with establishing modular open system guidance and policy for multiple customers.

Dr. Bail's technical areas of focus include dependable software design and assessment, metric definition and application, error handling policies, techniques for software specification development, design methodologies, metric definition and application, and verification and validation. Prior to 1990, Dr. Bail worked at Intermetrics Inc. in Bethesda MD.

From 1989 to 2011, he served as a part-time Adjunct Professor at the University of Maryland University College where he developed instructional materials and taught courses in software engineering, in topics such as Software Requirements, Verification and Validation, Software Design, Software Engineering, Fault Tolerant Software, and others. Previously, Dr. Bail taught part-time at The University of Maryland from 1983-1986 in the Computer Science Department for undergraduate courses in discrete mathematics, computer architecture, and programming language theory.

Dr. Bail has presented tutorials on Cleanroom Software Engineering, Semi-Formal Development Techniques, Statistical Testing, Verification and Validation, and Requirements Engineering at SIGAda, AdaEurope, NDIA Systems Engineering Conference, and other conferences.

Dr. Bail received a BS in Mathematics from Carnegie Institute of Technology, and an MS and Ph.D. in Computer Science from the University of Maryland.

T6 - Scheduling analysis of AADL architecture models

Frank Singhoff, Lab-STICC/UBO
Pierre Dissaux, Ellidiss Technologies

Location: Ruby 1 Room

In this tutorial, we will provide an overview of scheduling analysis capabilities that are proposed by thereal-ti me scheduling theory, AADL and tools implementing it. The objective of this tutorial is to show to the attendees the benefits that can be expected by performing early scheduling/timing analysis for real-time software.

The Architecture Analysis and Design Language (AADL) is an SAE International Standard dedicated to 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.

14 years after the first release of the AADL standard, the AADL community has implemented many AADL tools that are mature enough to be handled by embedded critical real-time systems designers. Then, we propose in this tutorial to show how to apply AADL scheduling analysis tools. The tutorial will be illustrated by AADL models and labs with the tools AADLInspector and Cheddar.

Cheddar is a GPL open-source scheduling analysis tool (http://beru.univ-brest.fr/~singhoff/cheddar). It has been designed and distributed to allow users to understand the main concepts of the real-time scheduling theory. The tool is built around a simplified Architecture Description Language devoted to support real-time constructs. Users can directly build their real-time systems models with this ADL and its associated editor, however, it is expected that other more general modeling front-ends have to be used while integrating scheduling analysis into an engineering process.

AADLInspector (http://www.ellidiss.fr) is a model processing framework that embeds a set of generic features to load real-time models and let them be properly processed by various analysis or production tools. AADLInspector uses AADL V2 standard as a base reference for its input models and embeds a commercial version of Cheddar as well as the interactive Marzhin simulator that emulates the AADL run-time.

The tutorial will illustrate how to model typical real-time architectures with AADL V2 and how to analyse them with AADLInspector/Cheddar (both the GPL version and the commercial version embedded into AADLInspector).
The tutorial will have the form of a lecture, with exercises/hand-outs and tools made available to participants. The speakers will come with virtual machines to allow attendees to run the tools and to do the exercises. For participants who cannot or do not want running the tools, the speakers will organize demonstrations and an interactive discussion while enriching the various models.

Level: Intermediate

The tutorial is designed for attendees who have no background on AADL nor scheduling analysis. Modelling and verification background may help.

Reasons for attending

AADL is notation which is part of the model-based families, along with OMG SysML, MARTE or EASTADL. 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.
Furthermore, scheduling analysis is not used as much it could be, because many practitioners may find it difficult to apply. The motivation of the tutorial is to highlight the level of maturity of the real-time modelling and analysis solutions around AADL, which is an outcome of the past ten years of academic and industrial research work in this area.

Presenters
 
Frank Singhoff (UBO/Lab-STICC, Brest, France) is Professor of Computer Science in the Lab-STICC laboratory, UMR CNRS 6285 and in the Computer Science Department at the Université de Bretagne Occidentale, France. He received his engineering degree in Computer Science from the CNAM/Paris in 1996 and his PhD from Télécom-Paris-Tech in 1999. His current research focuses on real-time scheduling analysis and architecture description languages on multi and many cores. In 2002, he started Cheddar, a toolset designed to perform analysis with the real-time scheduling theory. Frank Singhoff is also a member of the SAE AS-2C committee working on the AADL. He received an ACM SIGAda “Outstanding Ada Community Contributions Award” in 2010. Frank Singhoff gave several tutorials at ESWEEK in 2013, MODELS in 2014, HILT in 2014, SIGAda in 2011 and 2007, Ada-Europe/RST in 2008, ETR in 2017, 2015 and 2009.

Pierre Dissaux has an engineering degree in electronics and is the owner and managing director of Ellidiss Technologies. Before founding the company in 2004, he held various job positions in a large telecommunication company (1983-1985), in a research center of the French Ministry of Defense (1985-1991) and in an innovating software house (1991-2003). He is also a member of the SAE AS-2C standardisation committee (AADL) and the main architect of the AADL Inspector tool.

T7 - Writing Contracts in Ada

Location: Ruby 2 Room

Jacob Sparre Andersen, JSA Research & Innovation

One of the important, new features in Ada 2012 was an extended support for contract-based programming with “contract aspects”. They allow you to specify even more details about types and subprograms in a formal and testable form. If used carefully, they can make package specifications easier to read, and help identifying use and implementation errors faster.

To really make sense, the contracts should be consistent across your whole library or application. This tutorial will introduce you to writing contracts in Ada and give you guidance on writing consistent contracts. It is organised in three sections: An introduction to writing contracts in Ada using features all the way from Ada 83 to Ada 2012/TC1. Guidelines for writing contracts. And, finally, a guided, practical exercise in writing contracts in Ada.

Level: Intermediate

The intended audience is software engineers, who already know an earlier version of Ada, but have not yet used the “programming by contract” aspects added in Ada 2012.

Reasons for attending

After having completed the tutorial, the participants will be ready to apply contract aspects on a project in a consistent and effective manner.
The tutorial is intended to prepare existing Ada programmers to use Ada 2012 contract aspects, both in future projects and on existing Ada projects.

Preparations

It is advised that the attendees bring laptops with an Ada 2012 compiler installed along for the tutorial.

Presenter
 
Jacob Sparre Andersen has previously given talks and tutorials on the use of Ada 2012 for contract-based programming at Ada-Europe conferences, as well as at DANSAS, FOSDEM and LinuxDay/Cagliari. He also has a long experience as a teacher of physics, mathematics, statistics, software engineering, and financial instruments.
Jacob Sparre Andersen runs his own consulting company in Hørsholm, Denmark and is an associate at the Niels Bohr Institute at University of Copenhagen. He is specialised in mathematical modelling and (of course) Ada. See http://www.jacob-sparre.dk/cv/ for a full curriculum vitae.

T8 - Introduction to Libadalang

Raphaël Amiard, AdaCore
Pierre-Marie de Rodat, AdaCore

Location: Ruby 3 Room

This tutorial will introduce the Libadalang Ada source code analysis library, and the way it can be used to create source aware custom tools. It will cover:

•  How to use Libadalang for simple metrics using syntax.
• How to use Libadalang for simple metrics using semantic analysis.
• How to use Libadalang to perform automatic refactorings on your code-base based on a set of rules.
• How to use Libadalang to implement checkers for custom coding rules.

Attendees should bring a computer with the GNAT GPL 2017 installed. These are available for download from https://adacore.com/download.

Level: Intermediate

No prior experience with Libadalang is expected, but attendees should be familiar with Ada. A modicum of familiarity with Python or another scripting language is a plus, but definitely not a requirement.

Reasons for attending

• Learn about creating custom Ada tooling easily.
• Learn about the main differences between Libadalang and ASIS.
• See real world uses of custom made source analysis technology.

Presenters
 
Raphaël Amiard is a software engineer at AdaCore working on tooling and compiler technologies. He joined AdaCore in 2013, after an internship on AdaCore’s IDEs. His main interests are compiler technologies, language design, and sound/music making.

Pierre-Marie joined AdaCore in 2013, after he got an engineering degree at EPITA (IT engineering school in Paris). He mainly works on GNATcoverage, GCC, GDB and Libadalang.

T9 - Unit-testing with Ahven

Jacob Sparre Andersen, JSA Research & Innovation

Location: Ruby 2 Room

Testing is a useful activity, even when you don’t have authorities breathing down your neck to document that you know what your software is doing.

Ahven is an Open Source framework for writing unit tests. It is intended to work with any Ada 95 compiler and is regularly tested with several different compilers.

This tutorial will introduce you to writing unit tests with Ahven as the testing framework. You will learn how to write simple tests, how to structure larger test suites, and how you can measure statement coverage of your unit tests with GNAT and Gcov.

Level: Intermediate

The intended audience is software engineers, who already know Ada, and are interested in a lightweight alternative to the unit testing tools used for certification purposes.

Reasons for attending

The tutorial will give you a good start writing unit tests, without tying you to a specific Ada compiler, or requiring you to pay license fees for one of the more advanced closed source Ada unit testing tools.

Preparations

It is advised that each attendee brings a laptop with an Ada 95 compiler (or newer) installed along for the tutorial. Attendees are welcome to bring some of their own Ada sources to use for the exercises.

Presenter
 
Jacob Sparre Andersen has previously given talks and tutorials on the use of Ada 2012 for contract-based programming at Ada-Europe conferences, as well as at DANSAS, FOSDEM and LinuxDay/Cagliari. He also has a long experience as a teacher of physics, mathematics, statistics, software engineering, and financial instruments.
Jacob Sparre Andersen runs his own consulting company in Hørsholm, Denmark and is an associate at the Niels Bohr Institute at University of Copenhagen. He is specialised in mathematical modelling and (of course) Ada. See http://www.jacob-sparre.dk/cv/ for a full curriculum vitae.

T10 - Frama-C, a Framework for Analysing C Code

Julien Signoles, CEA LIST

Location: Ruby 3 Room

The last few decades have seen much of the groundwork of formal software analysis being laid. Several angles and theoretical avenues have been explored, from deductive verification to abstract interpretation to program transformation to monitoring. While much remains to be done from an academic standpoint, these techniques have become mature enough to have been successfully implemented and used in industrial settings.

In this context, verification of C programs is of the utmost importance because the C programming language is still the language of choice for developing safety-critical systems and is also routinely used for security-based applications. However, verifying large C programs remains a time-consuming and challenging task. One of the reasons is related to the C programming language itself, because it combines high level features like arrays and low level features like user-controlled memory allocations, bitfields and unions. Another reason comes from weaknesses of each verification technique: dynamic techniques are not bothered by C code complexity but are not exhaustive, abstract interpretation is exhaustive and almost automatic but may be imprecise and cannot verify complex functional properties, while deductive methods may tackle a broad varieties of properties but require formal specifications and may be less efficient in presence of low level code. One effective way to circumvent this problem is to combine several analyses in order to reduce weaknesses of each one thanks to the others. For instance, abstract interpretation can ensure the absence of most runtime errors, deductive verification can prove most functional properties, while monitoring can check at runtime the remaining properties. Such analysis combinations is the raison d'être of Frama-C.

The Frama-C software analysis platform provides a collection of scalable, interoperable, and sound software analyses for the industrial analysis of ISO C99 source code. The platform is based on a kernel which hosts analyzers as collaborating plug-ins and uses the ACSL formal specification language as a lingua franca. Frama-C includes plug-ins based on abstract interpretation, deductive verification and runtime verification, as well as a series of derived plug-ins which build elaborate analyses upon the basic ones. This large variety of analysis techniques and its unique collaboration capabilities make Frama-C most suitable for developing new code analyzers and applying code analysis techniques in many academic and industrial projects. For instance, Frama-C is currently used by several actors of the avionic, nuclear and defense industries.

This 3-hour tutorial brings participants to a journey into the Frama-C world along its main plug-ins. It aims at providing the essence of each technique and tool along with a few illustrating examples. After a general overview of Frama-C, it presents the deductive verification tool WP together with the formal specification language ACSL, the abstract interpretation based plug-in Eva and its derived plug-ins, and the runtime verification tool E-ACSL as well as a few possible combinations of plug-ins.

Level: Introductory / Intermediate

Attendees should know the C programming language but no former experience with formal methods is required.

Reasons for attending

• If you don’t know formal methods: learn what they are (not) good for and how to use them concretely.
• 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 for analysing critical C software.

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