Tutorials

Morning tutorial sessions will start at 9:00 and end at 12:30. Afternoon sessions will start at 14:00 and end at 17:30. There will be coffee breaks at 10:30 - 11:00 and at 15:30 - 16:00. 

T1: Advanced Ada Support for Real-Time Programming

Mario Aldea Rivas, Universidad de Cantabria, Spain

The support of Ada for real-time programming has experienced a large improvement in the last years. Functionalities such as hierarchical scheduling based on priority bands, new dispatching policies, execution time clocks and timers, timing events, etc. are in the standard from Ada 2005 but they have not gotten the relevance that they deserve due to the lack of free software implementations. Most of these relatively new services are starting to be available in some platforms. In particular, in this tutorial we will use the MaRTE OS/GNAT platform. The tutorial will give a practical introduction to most of these relatively underused real-time services. Along with the description of every service we will provide some examples in the form of typical use patterns.

Level
Intermediate. Target audience: Practitioners of real-time systems interested in learning about the newest Ada real-time support and how to use it in its applications. Previous knowledge of general Ada programming is assumed.

Reasons for attending
Attendees will increase their knowledge about the great support of Ada for real-time programming and they will be able to take advantage of it in their applications.
 

Presenter

Mario Aldea Rivas is an Associate Professor in the Department of Mathematics, Statistics and Computer Science at the Universidad de Cantabria. He works in software engineering for real-time systems, and particularly in flexible scheduling, real-time operating systems, and real-time languages. He has been involved in several industrial projects using Ada to build real-time controllers for robots. Mario is the developer of MaRTE OS an operating system that has served as platform to provide support for the most advanced Ada real-time services.

T2: Developing High-Integrity Systems with GNAT GPL and the Ravenscar Profile

Juan A. de la Puente and Juan Zamorano, Universidad Politécnica de Madrid, Spain

The tutorial will summarise the main aspects of the Ravenscar profile, as well as some other basic real-time facilities available in Ada 2012. Programming patterns for analysable real-time systems will be described, together with software development techniques for high-integrity systems. The use of the GNAT GPL for the LEGO MINDSTORMS NXT toolchain will be described in the context of a comprehensive example. A LEGO MINDSTORMS NXT robot will be used as a platform for the use of cross-development and debugging tools.

Level
Intermediate. The tutorial is aimed at project managers, systems engineers, and developers of critical software systems.

Reasons for attending
Attendants will learn the main concepts and techniques needed to develop high-integrity real-time systems on a representative platform for robotic applications. A LEGO MINDSTORMS NXT will be used for a comprehensive example of software development using GNAT GPL for LEGO MINDSTORMS NXT.

Juan Antonio de la Puente is a professor at the Universidad Politécnica de Madrid (UPM). He has been teaching Ada and Real-Time systems for more than 20 years. As the head of the real-time systems group at UPM, he has led the development and evolution of the Open Ravenscar real-time Kernel (ORK) for the last 10 years and the work in UPM on GNAT GPL for LEGO MINDSTORMS NXT, that includes the porting to Linux/GNU hosts as well as integrating tools for developing real-time embedded software.

Juan Zamorano is an assistant professor at the Universidad Politécnica de Madrid (UPM), with more than 20 years experience in teaching real-time systems and computer architecture. He is the technical manager of the ORK project, and is responsible for ORK maintenance at UPM and the work in UPM on GNAT GPL for LEGO MINDSTORMS NXT, that includes the porting to Linux/GNU hosts as well as integrating tools for developing real-time embedded software.

T3: How to Optimize Reliable Software

Ian Broster and Andrew Coombes, Rapita Systems Ltd, UK

Software timing is important in reliable systems, but what can we do when it's wrong? There are many common misconceptions and pitfalls in approaches to solving timing problems, which consume effort and resources while failing to address the underlying issues. In this tutorial, we explain an effective process that avoids these pitfalls. This process identifies code that contributes the most to the overall worst-case execution time, asks “what if” questions about the outcome of optimization, and targets optimization effort where it will have the maximum benefit for the minimum cost. The tutorial closes with a summary of the results of case study, applying this process to a large Ada project. There will be an opportunity for hands-on work, including a competition and prize for the best optimization.

Level
Intermediate. This tutorial is aimed at general embedded engineers and managers who have the desire to develop reliable embedded software,

Reasons for attending
This tutorial will benefit embedded software developers and managers who need to engineer reliable, embedded software. The presentation covers two key aspects of real-time systems performance: (1) how to gain a clear, detailed, and accurate understanding of the execution time behavior of embedded software, (2) how to target optimization effort precisely where it will have the maximum benefit in improving system timing behavior (eliminating timing failures and creating headroom for new functionality) for the minimum cost. 

Presenters

Dr Ian Broster is a founder and Director of Rapita Systems Ltd, a company specializing in software timing analysis. He is an experienced, lively lecturer who has given numerous training courses, lectures and presentations on this and other topics. He has been involved with Ada for several years. He earned his PhD at the Real-Time Systems Research Group of University of York.

Dr Andrew Coombes runs the Marketing and Engineering Services groups at Rapita Systems Ltd. For the last 13 years he has been involved in the development and commercialization of software tools for embedded, real-time applications. Prior to this, he worked in a consultancy and for the BAE Systems DCSC (Dependable Computing Systems Centre). He received his DPhil in Computer Science at the High-Integrity Systems Engineering Group at the University of York. He has run training courses and given presentations at many international conferences.

T4: DO-178C: The Next Avionics Software Safety Standard

Ben Brosgol, AdaCore, USA

The DO-178B (ED-12B) avionics software safety standard has recently been revised, to take into account nearly 20 years of experience and to provide specific guidance on several development approaches and technologies that are seeing increasing usage both in general and for avionics systems in particular. The revised standard, known as RTCA DO-178C (or EUROCAE ED-12C), was completed in December 2011. It comprises a Core document as well as several supplements: Software Tool Qualification Considerations, Model-Based Development and Verification, Object-Oriented Technology and Related Techniques, and Formal Methods.

This tutorial will cover the Core document, with a focus on the objectives and activities associated with the software verification process. It will also summarize the various supplements, explain the new guidance concerning the usage of Object-Oriented Technology, and briefly describe how security considerations are being addressed.

Level
Intermediate. Some experience with software development processes in general and Object-Oriented technology in particular is assumed.  No previous experience with DO-178B, or with avionics application programming, is required.

Reasons for attending
Attendees will learn essential information about DO-178C including:
- The differences between process-based and goal-based safety standards
- The activities and evidence required to demonstrate safety certification
- The role of testing in software verification
- The approaches to MC/DC, including a variation (“masking MC/DC”) explicitly permitted in DO-178C
- The significance of the Liskov Substitution Principle in verifying Object-Oriented software
- The new approach to tool qualification
- How security issues are being taken into account

Presenter

Dr. Benjamin Brosgol is a senior member of the technical staff of AdaCore. He has been involved with programming language design and implementation for more than 30 years, concentrating on languages and technologies for high-integrity systems. Dr. Brosgol has presented papers and tutorials on safety and security certification on numerous occasions including Ada-Europe, ACM SIGAda, ESC (Embedded Systems Conference), ICSE (IEEE/ACM International Conference on Software Engineering), and SSTC (Systems & Software Technology Conference). Dr. Brosgol holds a BA in Mathematics from Amherst College, and MS and PhD degrees in Applied Mathematics from Harvard University.

T5: Designing and Checking Coding Standards for Ada

Jean-Pierre Rosen, Adalog, France

Most companies have developed coding standards (often because having one is a requirement for certification), but few have conducted a real analysis of the value, consistency, and efficiency of the coding standard. This tutorial presents the challenges of establishing a coding standard, not just for the sake of having one, but with the goal of actually improving the quality of software. This implies not only having "good" rules, but also having rules that are understood, accepted, and adhered to by the programming team. The issue of automatically checking the rules is also fundamental: experience shows that no manual checking can cover the programming rules to a satisfactory extent. The tutorial presents the tools available, and criteria for choosing such a tool.

Level
Intermediate. Expected audience experience: No special requirement.

Reasons for attending
- Understand the value of coding standards
- Learn how to choose you own coding rules, in a way that's both useful and efficient.
- Consider the difficulties and pitfalls of introducing coding standard to the development teams, and how to overcome them.

Presenter

JP 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.

T6: Experimenting with ParaSail – Parallel Specification and Implementation Language

Tucker Taft, SofCheck div. of AdaCore, USA

This tutorial will allow experimentation with a prototype compiler and virtual machine for ParaSail, a new language designed to support the safe, secure, and productive development of parallel programs. ParaSail has pervasive parallelism along with extensive compile-time checking of annotations in the form of assertions, preconditions, postconditions, etc. ParaSail does all checking at compile time, and eliminates race conditions, null dereferences, uninitialized data access, numeric overflow, out of bounds indexing, etc. as well as statically checking the truth of all user-written assertions. After a short introduction to the language, attendees will receive a prototype ParaSail compiler and an accompanying ParaSail Virtual Machine interpreter for writing and testing ParaSail programs. The tutorial will finish with a group discussion and feedback on the experience of using this new language.

Level
The tutorial includes an introduction to the language.  No specific prerequisites other than an interest and ability in learning a new language, plus a basic understanding of parallelism, assertions, preconditions, and postconditions.

Reasons for attending
This is a chance to experiment with a new programming language oriented around parallelism and formal verification.  The language is still quite new, so it is also a chance to provide feedback on the language, and perhaps gain some insights that might contribute to other language design efforts.

Presenter

The presenter has been involved with language design since 1975, and with Ada since 1980. He was the technical lead for the design of Ada 95, and was heavily involved in the design of Ada 2005 and the forthcoming Ada 2012. In addition to language design, the presenter has been the technical lead on the development of an Ada 83 and of an Ada 95 compiler, as well as of an advanced language-independent static analysis technology. Since 2009, the presenter has been developing the ParaSail language and a prototype implementation.

T7: Basics of Oracle Database Programming with Ada: Introduction to the Konada.Db Library (morning)
 
T8: Oracle Database GUI-programming on MS Windows (afternoon)

Frank Piron, KonAd GmbH, Germany

The tutorial gives an introduction to Oracle Database Programming with Ada. Based on the Konada.Db library and the GWindows extensions made by KonAd it will be shown how to develop GUI and non-GUI Oracle Database Applications or to enhance existing applications with Oracle Database connectivity. Except the Ada libraries only the Oracle Call Interface library and (for GUI-Applications) the Win32 API is needed.

The tutorial will be divided in two parts, which can be taken independently, with the morning session devoted to Oracle programming, with command line programs which are operating system independent, and the afternoon session integrating the GUI components for Microsoft Windows.

Level
The tutorial is directed to Ada developers who want to extend their applications with Oracle Database connectivity in a pure Ada Way without using JDBC or ODBC nor using other third party libraries except the Oracle Call Interface.
The attendees of the tutorial are excpected to have intermediate experience in Ada development and a basic unterstanding of what database programming is. For example they should know about SQL, relational Databases and transactions. Special knowledge about Oracle Databases would be helpful but is not necessary.
If interested in the GUI-part of the tutorial the attendees should know the basics of Windows GUI-development concepts e.g. the message loop, controls, callbacks, window management etc.

Reasons for attending
- Learning how to use the freely available Konada.Db basic library.
- Extending Ada programs with Oracle Database interaction - with or without a GUI-part. If the programs do not contain a GUI-part then this is possible on any Ada and OCI aware platform. This includes Linux, Solaris and MS Windows.
- With the GUI-part this approach may be an alternative direction for Oracle Forms Developers to go. Making the transition easier because of the similarity between Ada and PL/SQL. The GUI-binding is available only for MS Windows.
- Enhancing an AWS (Ada Web Server) application with Oracle Database access.

Presenter

Frank Piron graduated in 1986 from the University of Bonn. From 1987 – 1991 worked at the Computer Science Department of the RWTH-Aachen including Tutorials and Seminars in Computer Science. Since 1997 he is a Database developer. He is co-founder of the KonAd GmbH. Data Warehousing Projects with the Deutsche Post AG included giving tutorials for Database Administrators and Developers in PL/SQL and Oracle Perfomance tuning. Since 2002 Ada he has been involved with the programming and development of the Konada.Db Framework. From 2003 – 2005 he developed the KWfl/ElSch Workflow and Document Management System which runs until now in a production environment in the city of Zurich. Since 2005 he further developed the Konada.Db framework.

T9: The Benefits of Using SPARK for High-assurance Software (morning)
 
T10: The Use of Proof and Generics in SPARK (afternoon)

Trevor Jennings, Altran Praxis, UK

SPARK is a contract-based sub-language of Ada which is unambiguous and suitable for rigorous static analysis. It has been extensively used in industrial applications where safety and security are paramount. The tutorial will begin with an introduction to SPARK for those who are unfamiliar with the language. We then consider simple examples of the proof of properties in SPARK programs. In particular we will look at the proof of absence of runtime exceptions. We explain the use of the proof tools, including the new counter-example finding tool, Riposte. The language and tools now support generics, so we will see how to use generics in SPARK to provide reusable components. Finally, we will consider proof of properties of these generic units with the SPARK proof tools.

The tutorial will be divided in two parts, which can be taken independently, with the morning session devoted to SPARK programming, and the afternoon session dedicated to recent features such as the Riposte tool and generics support.

Level
The level of the tutorial is intermediate. The recommended experience and background of the audience are practising software engineers, programme managers, and those involved with procurement of high-integrity software systems might attend this tutorial. Some background in the development of safety- or security-critical software might be useful, but not essential. The audience should not be put off by the fact that we discuss program proof. The examples used will be simple and accessible. The afternon part expects previous knowledge of SPARK (provided in the morning).

Reasons for attending
- To learn about the trade-offs in the design of programming languages and static analysis tools.
- To learn about what such tools can and can't offer in terms of soundness, depth, efficiency and completeness of analysis.
 -To appreciate the SPARK language, and the capabilities of the SPARK toolset.
- To gain an understanding of automated program proof and how it is done in SPARK
- To learn about new developments in SPARK such as generics and counter-example finding.
- To discuss possible extensions to SPARK to incorporate new features from Ada 2012.

Presenter

Trevor is a Fellow of the British Computer Society with over 40 years of experience in the computer industry, both in hardware and software roles. His involvement with Ada started in 1979 during his postgraduate research at The City University in London. Whilst a research fellow at Southampton University between 1986 and 1989, he developed SPARK, an annotated subset of Ada specifically designed for deep static analysis for use in high-assurance systems and co-authored its first published definition. He is now a member of the SPARK team, developing and supporting the SPARK Toolset. He regularly presents SPARK training courses.

T11: Design of Multitask Software: the Entity-Life Modeling Approach

Bo Sandén, Colorado Technical University, USA

The tutorial introduces entity-life modeling (ELM). It is a design approach for multitask, reactive software, that is software that responds to events in the environment as they occur. It is not a multi-step method but rather an extension of object orientation into the time dimension: the central idea is that the task architecture should reflect concurrency that exists in the problem. The tutorial follows the presenter’s recent book Design of multithreaded software: The entity-life modeling approach (IEEE Computer Society/Wiley 2011) but uses Ada terminology. ELM was originally developed with Ada tasking in mind but works with Real-time Java as well. The tutorial is illustrated with multiple Ada examples.

Level
Intended for architects, designers, and programmers of real-time and interactive software as well as software-engineering academics and students interested in concurrency. 
If tasking is considered an “advanced” aspect of Ada, the level of the tutorial is advanced. It assumes general knowledge of tasking or threading.

Reasons for attending
Understand and eventually learn the ELM way of designing reactive, multitask software.

Presenter

Dr. Bo Sandén began his career as a software developer in industry and had the opportunity to study and design multithreaded software. 1986-87 he was a Visiting Associate Professor in the pioneering software-engineering program at the Wang Institute, Tyngsboro, MA. As an Associate Professor at George Mason University, Fairfax, VA 1987-1996, he helped create a masters program in software systems engineering. Since 1996 he is a Professor of Computer Science at Colorado Technical University in Colorado Springs, where he has taught at the undergraduate and master’s levels and now exclusively teaches and directs student research in the Doctor of Computer Science program. Dr. Sandén is the inventor of entity-life modeling. He gave a number of tutorials on ELM in the mid-90s: ACM Professional Development Seminar 1994, Washington Ada Symposium 1994, 1995, 1996; TRI-Ada 1994, 1995, 1996. Since then he has taught ELM at Colorado Tech and externally, and published a number of articles on the topic primarily in the IEEE magazines. He holds an MS in Engineering Physics from Lund Institute of Technology and a Ph.D. in Information Processing from the Royal Institute of Technology, Stockholm.